Metamath Proof Explorer

Theorem ensn1g

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004)

Ref Expression
Assertion ensn1g 
|- ( A e. V -> { A } ~~ 1o )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = A -> { x } = { A } )
2 1 breq1d 
 |-  ( x = A -> ( { x } ~~ 1o <-> { A } ~~ 1o ) )
3 vex 
 |-  x e. _V
4 3 ensn1 
 |-  { x } ~~ 1o
5 2 4 vtoclg 
 |-  ( A e. V -> { A } ~~ 1o )