Theorem snprc 4717

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 4642	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4352	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3494	. . 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 3480  ∅c0 4333  {csn 4626

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 2708

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 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-nul 4334  df-sn 4627

This theorem is referenced by:  snnzb  4718  rmosn  4719  rabsnif  4723  prprc1  4765  prprc  4767  preqsnd  4859  unisn2  5312  eqsnuniex  5361  snexALT  5383  snex  5436  posn  5771  frsn  5773  relsnb  5812  relimasn  6103  elimasni  6109  inisegn0  6116  dmsnsnsn  6240  predprc  6359  sucprc  6460  dffv3  6902  fconst5  7226  ordsuci  7828  1stval  8016  2ndval  8017  ecexr  8750  snfi  9083  snfiOLD  9084  domunsn  9167  snnen2oOLD  9264  hashrabrsn  14411  hashrabsn01  14412  hashrabsn1  14413  elprchashprn2  14435  hashsn01  14455  hash2pwpr  14515  snsymgefmndeq  19412  efgrelexlema  19767  usgr1v  29273  1conngr  30213  frgr1v  30290  n0lplig  30502  unidifsnne  32554  eldm3  35761  opelco3  35775  fvsingle  35921  unisnif  35926  funpartlem  35943  bj-sngltag  36984  bj-snex  37036  bj-restsnid  37088  bj-snmooreb  37115  wopprc  43042  safesnsupfidom1o  43430  sn1dom  43539  uneqsn  44038  vsn  48731  mofsn2  48754