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	⊢ ( 𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2	1	brrelex1i	⊢ ( 𝑆 ≈ 1o → 𝑆 ∈ V )
3		uniexg	⊢ ( 𝑆 ∈ V → ∪ 𝑆 ∈ V )
4		snidg	⊢ ( ∪ 𝑆 ∈ V → ∪ 𝑆 ∈ { ∪ 𝑆 } )
5	2 3 4	3syl	⊢ ( 𝑆 ≈ 1o → ∪ 𝑆 ∈ { ∪ 𝑆 } )
6		en1b	⊢ ( 𝑆 ≈ 1o ↔ 𝑆 = { ∪ 𝑆 } )
7	6	biimpi	⊢ ( 𝑆 ≈ 1o → 𝑆 = { ∪ 𝑆 } )
8	5 7	eleqtrrd	⊢ ( 𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆 )