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

Proof

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