Theorem en1uniel

Description: A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

	Ref	Expression
Assertion	en1uniel	$$⊢S\approx 1_{𝑜}\to \bigcup S\in S$$

Proof

Step	Hyp	Ref	Expression
1		en1b	$$⊢S\approx 1_{𝑜}\leftrightarrow S=\left\{\bigcup S\right\}$$
2		eqsnuniex	$$⊢S=\left\{\bigcup S\right\}\to \bigcup S\in \mathrm{V}$$
3	1 2	sylbi	$$⊢S\approx 1_{𝑜}\to \bigcup S\in \mathrm{V}$$
4		snidg	$$⊢\bigcup S\in \mathrm{V}\to \bigcup S\in \left\{\bigcup S\right\}$$
5	3 4	syl	$$⊢S\approx 1_{𝑜}\to \bigcup S\in \left\{\bigcup S\right\}$$
6	1	biimpi	$$⊢S\approx 1_{𝑜}\to S=\left\{\bigcup S\right\}$$
7	5 6	eleqtrrd	$$⊢S\approx 1_{𝑜}\to \bigcup S\in S$$