Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

	Ref	Expression
Assertion	en1b	$$⊢A\approx 1_{𝑜}\leftrightarrow A=\left\{\bigcup A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		en1	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$
2		id	$$⊢A=\left\{x\right\}\to A=\left\{x\right\}$$
3		unieq	$$⊢A=\left\{x\right\}\to \bigcup A=\bigcup \left\{x\right\}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	unisn	$$⊢\bigcup \left\{x\right\}=x$$
6	3 5	eqtrdi	$$⊢A=\left\{x\right\}\to \bigcup A=x$$
7	6	sneqd	$$⊢A=\left\{x\right\}\to \left\{\bigcup A\right\}=\left\{x\right\}$$
8	2 7	eqtr4d	$$⊢A=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
9	8	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A=\left\{\bigcup A\right\}$$
10	1 9	sylbi	$$⊢A\approx 1_{𝑜}\to A=\left\{\bigcup A\right\}$$
11		id	$$⊢A=\left\{\bigcup A\right\}\to A=\left\{\bigcup A\right\}$$
12		eqsnuniex	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A\in \mathrm{V}$$
13		ensn1g	$$⊢\bigcup A\in \mathrm{V}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
14	12 13	syl	$$⊢A=\left\{\bigcup A\right\}\to \left\{\bigcup A\right\}\approx 1_{𝑜}$$
15	11 14	eqbrtrd	$$⊢A=\left\{\bigcup A\right\}\to A\approx 1_{𝑜}$$
16	10 15	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow A=\left\{\bigcup A\right\}$$