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 1 𝑜 S S

Proof

Step Hyp Ref Expression
1 relen Rel
2 1 brrelex1i S 1 𝑜 S V
3 uniexg S V S V
4 snidg S V S S
5 2 3 4 3syl S 1 𝑜 S S
6 en1b S 1 𝑜 S = S
7 6 biimpi S 1 𝑜 S = S
8 5 7 eleqtrrd S 1 𝑜 S S