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	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
2	1	exbii	⊢ ( ∃ 𝑥 𝑥 ∈ { 𝐴 } ↔ ∃ 𝑥 𝑥 = 𝐴 )
3		neq0	⊢ ( ¬ { 𝐴 } = ∅ ↔ ∃ 𝑥 𝑥 ∈ { 𝐴 } )
4		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
5	2 3 4	3bitr4i	⊢ ( ¬ { 𝐴 } = ∅ ↔ 𝐴 ∈ V )
6	5	con1bii	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )