Theorem: SetTheory.eq_pair_iff (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = pair y z ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z
Tactic:
rw [ext_iff]
State after:
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

State before:
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
Tactic:
simp
State after:
no goals