rw [ext_iff]
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = pair y z ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ (∀ (z_1 : V), z_1 ∈ x ↔ z_1 ∈ pair y z) ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z