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 ¬ A V A =

Proof

Step Hyp Ref Expression
1 velsn x A x = A
2 1 exbii x x A x x = A
3 neq0 ¬ A = x x A
4 isset A V x x = A
5 2 3 4 3bitr4i ¬ A = A V
6 5 con1bii ¬ A V A =