Metamath Proof Explorer


Theorem snen1g

Description: A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023)

Ref Expression
Assertion snen1g A 1 𝑜 A V

Proof

Step Hyp Ref Expression
1 eqcom A = x x = A
2 vex x V
3 2 sneqr x = A x = A
4 sneq x = A x = A
5 3 4 impbii x = A x = A
6 1 5 bitri A = x x = A
7 6 exbii x A = x x x = A
8 en1 A 1 𝑜 x A = x
9 isset A V x x = A
10 7 8 9 3bitr4i A 1 𝑜 A V