Theorem snprc 4661

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 4583	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4292	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3443	. . 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 3429  ∅c0 4273  {csn 4567

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-nul 4274  df-sn 4568

This theorem is referenced by:  snnzb  4662  rmosn  4663  rabsnif  4667  prprc1  4709  prprc  4711  preqsnd  4802  unisn2  5247  eqsnuniex  5303  snexALT  5325  snexOLD  5384  posn  5717  frsn  5719  relsnb  5758  relimasn  6050  elimasni  6056  inisegn0  6063  dmsnsnsn  6184  predprc  6302  sucprc  6401  dffv3  6836  fconst5  7161  ordsuci  7762  1stval  7944  2ndval  7945  ecexr  8648  snfi  8990  domunsn  9065  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  elprchashprn2  14358  hashsn01  14378  hash2pwpr  14438  snsymgefmndeq  19370  efgrelexlema  19724  usgr1v  29325  1conngr  30264  frgr1v  30341  n0lplig  30554  unidifsnne  32606  eldm3  35943  opelco3  35957  fvsingle  36100  unisnif  36105  funpartlem  36124  bj-sngltag  37290  bj-snex  37342  bj-restsnid  37399  bj-snmooreb  37426  wopprc  43458  safesnsupfidom1o  43844  sn1dom  43953  uneqsn  44452  vsn  49287  mofsn2  49320