Theorem ensn1g

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

	Ref	Expression
Assertion	ensn1g	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
2	1	breq1d	$$⊢x=A\to \left(\left\{x\right\}\approx 1_{𝑜}\leftrightarrow \left\{A\right\}\approx 1_{𝑜}\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	ensn1	$$⊢\left\{x\right\}\approx 1_{𝑜}$$
5	2 4	vtoclg	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$