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	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow A\in \left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		snen1g	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow A\in \mathrm{V}$$
2		snidb	$$⊢A\in \mathrm{V}\leftrightarrow A\in \left\{A\right\}$$
3	1 2	bitri	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow A\in \left\{A\right\}$$