Description: A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | snen1g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom | ||
2 | vex | ||
3 | 2 | sneqr | |
4 | sneq | ||
5 | 3 4 | impbii | |
6 | 1 5 | bitri | |
7 | 6 | exbii | |
8 | en1 | ||
9 | isset | ||
10 | 7 8 9 | 3bitr4i |