Theorem ensn1g

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004)

	Ref	Expression
Assertion	ensn1g	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
2	1	breq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 } ≈ 1o ↔ { 𝐴 } ≈ 1o ) )
3		vex	⊢ 𝑥 ∈ V
4	3	ensn1	⊢ { 𝑥 } ≈ 1o
5	2 4	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o )