rw [ext_iff] at h
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : {x} ∪ pair x y = {x} ∩ pair x y
⊢ x = y
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ x = y