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

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢\left\{A\right\}=\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{A\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	sneqr	$$⊢\left\{x\right\}=\left\{A\right\}\to x=A$$
4		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
5	3 4	impbii	$$⊢\left\{x\right\}=\left\{A\right\}\leftrightarrow x=A$$
6	1 5	bitri	$$⊢\left\{A\right\}=\left\{x\right\}\leftrightarrow x=A$$
7	6	exbii	$$⊢\exists x\left\{A\right\}=\left\{x\right\}\leftrightarrow \exists xx=A$$
8		en1	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow \exists x\left\{A\right\}=\left\{x\right\}$$
9		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
10	7 8 9	3bitr4i	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow A\in \mathrm{V}$$