rw [opair, mem_pair_iff] at hz
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z ∈ opair a b
⊢ z ∈ power (x ∪ y)
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z = {a} ∨ z = pair a b
⊢ z ∈ power (x ∪ y)