simp only [sUnion_pair, sInter_pair, ne_eq, union_pair_eq_inter_pair]
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1,
      z ∈ z_1 ∧
        z_1 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) ↔ z ∈ y