Theorem: SetTheory.mem_singleton_iff (SetTheory/Axioms.lean)

State before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ {x} ↔ y = x
Tactic:
show y ∈ pair x x ↔ y = x
State after:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ pair x x ↔ y = x

State before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
y x : V
inst✝ : Pairing V
⊢ y ∈ pair x x ↔ y = x
Tactic:
simp
State after:
no goals