Metamath Proof Explorer

Theorem en0

Description: The empty set is equinumerous only to itself. Exercise 1 of TakeutiZaring p. 88. (Contributed by NM, 27-May-1998)

Ref Expression
Assertion en0 
|- ( A ~~ (/) <-> A = (/) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ (/) <-> E. f f : A -1-1-onto-> (/) )
2 f1ocnv 
 |-  ( f : A -1-1-onto-> (/) -> `' f : (/) -1-1-onto-> A )
3 f1o00 
 |-  ( `' f : (/) -1-1-onto-> A <-> ( `' f = (/) /\ A = (/) ) )
4 3 simprbi 
 |-  ( `' f : (/) -1-1-onto-> A -> A = (/) )
5 2 4 syl 
 |-  ( f : A -1-1-onto-> (/) -> A = (/) )
6 5 exlimiv 
 |-  ( E. f f : A -1-1-onto-> (/) -> A = (/) )
7 1 6 sylbi 
 |-  ( A ~~ (/) -> A = (/) )
8 0ex 
 |-  (/) e. _V
9 8 enref 
 |-  (/) ~~ (/)
10 breq1 
 |-  ( A = (/) -> ( A ~~ (/) <-> (/) ~~ (/) ) )
11 9 10 mpbiri 
 |-  ( A = (/) -> A ~~ (/) )
12 7 11 impbii 
 |-  ( A ~~ (/) <-> A = (/) )