This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elsng

Description: There is exactly one element in a singleton. Exercise 2 of TakeutiZaring p. 15 (generalized). (Contributed by NM, 13-Sep-1995) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion elsng ⊢ A ∈ V → A ∈ B ↔ A = B

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ x = A → x = B ↔ A = B
2 df-sn ⊢ B = x | x = B
3 1 2 elab2g ⊢ A ∈ V → A ∈ B ↔ A = B