Metamath Proof Explorer


Theorem en1b

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 A1𝑜A=A

Proof

Step Hyp Ref Expression
1 en1 A1𝑜xA=x
2 id A=xA=x
3 unieq A=xA=x
4 vex xV
5 4 unisn x=x
6 3 5 eqtrdi A=xA=x
7 6 sneqd A=xA=x
8 2 7 eqtr4d A=xA=A
9 8 exlimiv xA=xA=A
10 1 9 sylbi A1𝑜A=A
11 id A=AA=A
12 eqsnuniex A=AAV
13 ensn1g AVA1𝑜
14 12 13 syl A=AA1𝑜
15 11 14 eqbrtrd A=AA1𝑜
16 10 15 impbii A1𝑜A=A