Theorem snprc 4674

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 4596	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4304	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3454	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 356	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-nul 4286  df-sn 4581

This theorem is referenced by:  snnzb  4675  rmosn  4676  rabsnif  4680  prprc1  4722  prprc  4724  preqsnd  4815  unisn2  5257  eqsnuniex  5306  snexALT  5328  snex  5381  posn  5710  frsn  5712  relsnb  5751  relimasn  6044  elimasni  6050  inisegn0  6057  dmsnsnsn  6178  predprc  6296  sucprc  6395  dffv3  6830  fconst5  7152  ordsuci  7753  1stval  7935  2ndval  7936  ecexr  8640  snfi  8980  domunsn  9055  hashrabrsn  14295  hashrabsn01  14296  hashrabsn1  14297  elprchashprn2  14319  hashsn01  14339  hash2pwpr  14399  snsymgefmndeq  19324  efgrelexlema  19678  usgr1v  29329  1conngr  30269  frgr1v  30346  n0lplig  30558  unidifsnne  32611  eldm3  35955  opelco3  35969  fvsingle  36112  unisnif  36117  funpartlem  36136  bj-sngltag  37184  bj-snex  37236  bj-restsnid  37292  bj-snmooreb  37319  wopprc  43272  safesnsupfidom1o  43658  sn1dom  43767  uneqsn  44266  vsn  49057  mofsn2  49090