exact this.1.symm
case mp.refine_2
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
this : y = x ∧ y ∈ pair x y
⊢ x = y
no goals