Description: A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | en1uniel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relen | ||
2 | 1 | brrelex1i | |
3 | uniexg | ||
4 | snidg | ||
5 | 2 3 4 | 3syl | |
6 | en1b | ||
7 | 6 | biimpi | |
8 | 5 7 | eleqtrrd |