Metamath Proof Explorer


Theorem snprc

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 ¬AVA=

Proof

Step Hyp Ref Expression
1 velsn xAx=A
2 1 exbii xxAxx=A
3 neq0 ¬A=xxA
4 isset AVxx=A
5 2 3 4 3bitr4i ¬A=AV
6 5 con1bii ¬AVA=