Theorem snprc 4685

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 4607	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1875	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4313	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3477	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-nul 4295  df-sn 4592

This theorem is referenced by:  snnzb  4686  rmosn  4687  rabsnif  4691  prprc1  4733  prprc  4735  preqsnd  4825  unisn2  5274  eqsnuniex  5330  snexALT  5352  snexOLD  5411  posn  5745  frsn  5747  relsnb  5787  relimasn  6085  elimasni  6091  inisegn0  6098  dmsnsnsn  6218  predprc  6336  sucprc  6436  dffv3  6875  fconst5  7202  ordsuci  7803  1stval  7984  2ndval  7985  ecexr  8695  snfi  9036  domunsn  9111  hashrabrsn  14404  hashrabsn01  14405  hashrabsn1  14406  elprchashprn2  14428  hashsn01  14449  hash2pwpr  14509  snsymgefmndeq  19461  efgrelexlema  19815  usgr1v  29543  1conngr  30482  frgr1v  30559  n0lplig  30772  unidifsnne  32819  eldm3  36148  opelco3  36162  fvsingle  36305  unisnif  36310  funpartlem  36329  bj-sngltag  37503  bj-snex  37555  bj-restsnid  37612  bj-snmooreb  37639  wopprc  43642  safesnsupfidom1o  44028  sn1dom  44137  uneqsn  44636  vsn  49468  mofsn2  49501