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 } ~~ 1o <-> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		eqcom	|- ( { A } = { x } <-> { x } = { A } )
2		vex	|- x e. _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	|- ( E. x { A } = { x } <-> E. x x = A )
8		en1	|- ( { A } ~~ 1o <-> E. x { A } = { x } )
9		isset	|- ( A e. _V <-> E. x x = A )
10	7 8 9	3bitr4i	|- ( { A } ~~ 1o <-> A e. _V )