Metamath Proof Explorer

Theorem elsn

Description: There is exactly one element in a singleton. Exercise 2 of TakeutiZaring p. 15. (Contributed by NM, 13-Sep-1995)

Ref Expression
Hypothesis elsn.1 
|- A e. _V
Assertion elsn 
|- ( A e. { B } <-> A = B )

Proof

Step Hyp Ref Expression
1 elsn.1 
 |-  A e. _V
2 elsng 
 |-  ( A e. _V -> ( A e. { B } <-> A = B ) )
3 1 2 ax-mp 
 |-  ( A e. { B } <-> A = B )