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 ~~ 1o -> U. S e. S )

Proof

Step	Hyp	Ref	Expression
1		en1b	|- ( S ~~ 1o <-> S = { U. S } )
2		eqsnuniex	|- ( S = { U. S } -> U. S e. _V )
3	1 2	sylbi	|- ( S ~~ 1o -> U. S e. _V )
4		snidg	|- ( U. S e. _V -> U. S e. { U. S } )
5	3 4	syl	|- ( S ~~ 1o -> U. S e. { U. S } )
6	1	biimpi	|- ( S ~~ 1o -> S = { U. S } )
7	5 6	eleqtrrd	|- ( S ~~ 1o -> U. S e. S )