Theorem snen1el

Description: A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023)

	Ref	Expression
Assertion	snen1el	⊢ ( { 𝐴 } ≈ 1o ↔ 𝐴 ∈ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		snen1g	⊢ ( { 𝐴 } ≈ 1o ↔ 𝐴 ∈ V )
2		snidb	⊢ ( 𝐴 ∈ V ↔ 𝐴 ∈ { 𝐴 } )
3	1 2	bitri	⊢ ( { 𝐴 } ≈ 1o ↔ 𝐴 ∈ { 𝐴 } )