Theorem en1unielOLD

Description: Obsolete version of en1uniel as of 24-Sep-2024. (Contributed by Stefan O'Rear, 16-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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