Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | en1b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | en1 | |
|
2 | id | |
|
3 | unieq | |
|
4 | vex | |
|
5 | 4 | unisn | |
6 | 3 5 | eqtrdi | |
7 | 6 | sneqd | |
8 | 2 7 | eqtr4d | |
9 | 8 | exlimiv | |
10 | 1 9 | sylbi | |
11 | id | |
|
12 | eqsnuniex | |
|
13 | ensn1g | |
|
14 | 12 13 | syl | |
15 | 11 14 | eqbrtrd | |
16 | 10 15 | impbii | |