Metamath Proof Explorer

Theorem kardsn

Description: A singleton has cardinality one. (Contributed by BTernaryTau, 4-Jul-2026)

Ref Expression
Assertion kardsn 
|- ( A e. V -> ( kard ` { A } ) = ( kard ` 1o ) )

Proof

Step Hyp Ref Expression
1 ensn1g 
 |-  ( A e. V -> { A } ~~ 1o )
2 snex 
 |-  { A } e. _V
3 kardeng 
 |-  ( { A } e. _V -> ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o ) )
4 2 3 ax-mp 
 |-  ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o )
5 1 4 sylibr 
 |-  ( A e. V -> ( kard ` { A } ) = ( kard ` 1o ) )