Metamath Proof Explorer

Theorem cardnueq0

Description: The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion cardnueq0 
|- ( A e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) )

Proof

Step Hyp Ref Expression
1 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
2 1 ensymd 
 |-  ( A e. dom card -> A ~~ ( card ` A ) )
3 breq2 
 |-  ( ( card ` A ) = (/) -> ( A ~~ ( card ` A ) <-> A ~~ (/) ) )
4 en0 
 |-  ( A ~~ (/) <-> A = (/) )
5 3 4 bitrdi 
 |-  ( ( card ` A ) = (/) -> ( A ~~ ( card ` A ) <-> A = (/) ) )
6 2 5 syl5ibcom 
 |-  ( A e. dom card -> ( ( card ` A ) = (/) -> A = (/) ) )
7 fveq2 
 |-  ( A = (/) -> ( card ` A ) = ( card ` (/) ) )
8 card0 
 |-  ( card ` (/) ) = (/)
9 7 8 eqtrdi 
 |-  ( A = (/) -> ( card ` A ) = (/) )
10 6 9 impbid1 
 |-  ( A e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) )