Description: The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of Quine p. 48. (Contributed by NM, 21-Jun-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | snprc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velsn | |
|
2 | 1 | exbii | |
3 | neq0 | |
|
4 | isset | |
|
5 | 2 3 4 | 3bitr4i | |
6 | 5 | con1bii | |