rw [mem_power_iff]
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ∈ power (x ∪ y)
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y