Theorem snprc 4662

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-nul 4275  df-sn 4569

This theorem is referenced by:  snnzb  4663  rmosn  4664  rabsnif  4668  prprc1  4710  prprc  4712  preqsnd  4803  unisn2  5247  eqsnuniex  5298  snexALT  5320  snexOLD  5379  posn  5710  frsn  5712  relsnb  5751  relimasn  6044  elimasni  6050  inisegn0  6057  dmsnsnsn  6178  predprc  6296  sucprc  6395  dffv3  6830  fconst5  7154  ordsuci  7755  1stval  7937  2ndval  7938  ecexr  8641  snfi  8983  domunsn  9058  hashrabrsn  14325  hashrabsn01  14326  hashrabsn1  14327  elprchashprn2  14349  hashsn01  14369  hash2pwpr  14429  snsymgefmndeq  19361  efgrelexlema  19715  usgr1v  29339  1conngr  30279  frgr1v  30356  n0lplig  30569  unidifsnne  32621  eldm3  35959  opelco3  35973  fvsingle  36116  unisnif  36121  funpartlem  36140  bj-sngltag  37306  bj-snex  37358  bj-restsnid  37415  bj-snmooreb  37442  wopprc  43476  safesnsupfidom1o  43862  sn1dom  43971  uneqsn  44470  vsn  49299  mofsn2  49332