Description: A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | snelsingles.1 | ||
Assertion | snelsingles |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snelsingles.1 | ||
2 | isset | ||
3 | eqcom | ||
4 | 3 | exbii | |
5 | 2 4 | bitri | |
6 | 1 5 | mpbi | |
7 | sneq | ||
8 | 6 7 | eximii | |
9 | elsingles | ||
10 | 8 9 | mpbir |