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 e. _V <-> { A } = (/) )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( x e. { A } <-> x = A )
2	1	exbii	|- ( E. x x e. { A } <-> E. x x = A )
3		neq0	|- ( -. { A } = (/) <-> E. x x e. { A } )
4		isset	|- ( A e. _V <-> E. x x = A )
5	2 3 4	3bitr4i	|- ( -. { A } = (/) <-> A e. _V )
6	5	con1bii	|- ( -. A e. _V <-> { A } = (/) )