rw [mem_π₂_iff]
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ π₂ (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 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y