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	⊢ ( { 𝐴 } ≈ 1o ↔ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( { 𝐴 } = { 𝑥 } ↔ { 𝑥 } = { 𝐴 } )
2		vex	⊢ 𝑥 ∈ V
3	2	sneqr	⊢ ( { 𝑥 } = { 𝐴 } → 𝑥 = 𝐴 )
4		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
5	3 4	impbii	⊢ ( { 𝑥 } = { 𝐴 } ↔ 𝑥 = 𝐴 )
6	1 5	bitri	⊢ ( { 𝐴 } = { 𝑥 } ↔ 𝑥 = 𝐴 )
7	6	exbii	⊢ ( ∃ 𝑥 { 𝐴 } = { 𝑥 } ↔ ∃ 𝑥 𝑥 = 𝐴 )
8		en1	⊢ ( { 𝐴 } ≈ 1o ↔ ∃ 𝑥 { 𝐴 } = { 𝑥 } )
9		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
10	7 8 9	3bitr4i	⊢ ( { 𝐴 } ≈ 1o ↔ 𝐴 ∈ V )