This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ∅