Theorem snprc 4693

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.)

Assertion

Ref	Expression
snprc	⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Proof of Theorem snprc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		velsn 4617	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4327	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3473	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-nul 4309  df-sn 4602

This theorem is referenced by:  snnzb  4694  rmosn  4695  rabsnif  4699  prprc1  4741  prprc  4743  preqsnd  4835  unisn2  5282  eqsnuniex  5331  snexALT  5353  snex  5406  posn  5740  frsn  5742  relsnb  5781  relimasn  6072  elimasni  6078  inisegn0  6085  dmsnsnsn  6209  predprc  6327  sucprc  6429  dffv3  6871  fconst5  7197  ordsuci  7800  1stval  7988  2ndval  7989  ecexr  8722  snfi  9055  snfiOLD  9056  domunsn  9139  snnen2oOLD  9234  hashrabrsn  14388  hashrabsn01  14389  hashrabsn1  14390  elprchashprn2  14412  hashsn01  14432  hash2pwpr  14492  snsymgefmndeq  19374  efgrelexlema  19728  usgr1v  29181  1conngr  30121  frgr1v  30198  n0lplig  30410  unidifsnne  32463  eldm3  35724  opelco3  35738  fvsingle  35884  unisnif  35889  funpartlem  35906  bj-sngltag  36947  bj-snex  36999  bj-restsnid  37051  bj-snmooreb  37078  wopprc  43001  safesnsupfidom1o  43388  sn1dom  43497  uneqsn  43996  vsn  48738  mofsn2  48771