Metamath Proof Explorer

Theorem en1uniel

Description: A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion en1uniel 
|- ( S ~~ 1o -> U. S e. S )

Proof

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