constructor
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y ↔ x = y
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y → x = y

case mpr
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = y → {x} ∪ pair x y = {x} ∩ pair x y