Metamath Proof Explorer

Theorem cardennn

Description: If A is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013)

Ref Expression
Assertion cardennn 
|- ( ( A ~~ B /\ B e. _om ) -> ( card ` A ) = B )

Proof

Step Hyp Ref Expression
1 carden2b 
 |-  ( A ~~ B -> ( card ` A ) = ( card ` B ) )
2 cardnn 
 |-  ( B e. _om -> ( card ` B ) = B )
3 1 2 sylan9eq 
 |-  ( ( A ~~ B /\ B e. _om ) -> ( card ` A ) = B )