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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv | |
|
2 | breng | |
|
3 | 1 2 | syl | |
4 | 3 | ibi | |
5 | f1ocnv | |
|
6 | f1o00 | |
|
7 | 6 | simprbi | |
8 | 5 7 | syl | |
9 | 8 | exlimiv | |
10 | 4 9 | syl | |
11 | 0ex | |
|
12 | f1oeq1 | |
|
13 | f1o0 | |
|
14 | 11 12 13 | ceqsexv2d | |
15 | breng | |
|
16 | 11 11 15 | mp2an | |
17 | 14 16 | mpbir | |
18 | breq1 | |
|
19 | 17 18 | mpbiri | |
20 | 10 19 | impbii | |