Metamath Proof Explorer

Theorem en0r

Description: The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 encv 
 |-  ( (/) ~~ A -> ( (/) e. _V /\ A e. _V ) )
2 breng 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( (/) ~~ A <-> E. f f : (/) -1-1-onto-> A ) )
3 1 2 syl 
 |-  ( (/) ~~ A -> ( (/) ~~ A <-> E. f f : (/) -1-1-onto-> A ) )
4 3 ibi 
 |-  ( (/) ~~ A -> E. f f : (/) -1-1-onto-> A )
5 f1o00 
 |-  ( f : (/) -1-1-onto-> A <-> ( f = (/) /\ A = (/) ) )
6 5 simprbi 
 |-  ( f : (/) -1-1-onto-> A -> A = (/) )
7 6 exlimiv 
 |-  ( E. f f : (/) -1-1-onto-> A -> A = (/) )
8 4 7 syl 
 |-  ( (/) ~~ A -> A = (/) )
9 0ex 
 |-  (/) e. _V
10 f1oeq1 
 |-  ( f = (/) -> ( f : (/) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) ) )
11 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
12 9 10 11 ceqsexv2d 
 |-  E. f f : (/) -1-1-onto-> (/)
13 breng 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) ) )
14 9 9 13 mp2an 
 |-  ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) )
15 12 14 mpbir 
 |-  (/) ~~ (/)
16 breq2 
 |-  ( A = (/) -> ( (/) ~~ A <-> (/) ~~ (/) ) )
17 15 16 mpbiri 
 |-  ( A = (/) -> (/) ~~ A )
18 8 17 impbii 
 |-  ( (/) ~~ A <-> A = (/) )