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) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion en0 AA=

Proof

Step Hyp Ref Expression
1 encv AAVV
2 breng AVVAff:A1-1 onto
3 1 2 syl AAff:A1-1 onto
4 3 ibi Aff:A1-1 onto
5 f1ocnv f:A1-1 ontof-1:1-1 ontoA
6 f1o00 f-1:1-1 ontoAf-1=A=
7 6 simprbi f-1:1-1 ontoAA=
8 5 7 syl f:A1-1 ontoA=
9 8 exlimiv ff:A1-1 ontoA=
10 4 9 syl AA=
11 0ex V
12 f1oeq1 f=f:1-1 onto:1-1 onto
13 f1o0 :1-1 onto
14 11 12 13 ceqsexv2d ff:1-1 onto
15 breng VVff:1-1 onto
16 11 11 15 mp2an ff:1-1 onto
17 14 16 mpbir
18 breq1 A=A
19 17 18 mpbiri A=A
20 10 19 impbii AA=