Theorem snprc 4560

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 4488	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1829	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4229	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3449	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 304	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 358	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1522  ∃wex 1761   ∈ wcel 2081  Vcvv 3437  ∅c0 4211  {csn 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-nul 4212  df-sn 4473

This theorem is referenced by:  snnzb  4561  rmosn  4562  rabsnif  4566  prprc1  4608  prprc  4610  preqsnd  4696  unisn2  5107  snexALT  5174  snex  5223  posn  5523  frsn  5525  relsnb  5561  relimasn  5828  elimasni  5832  inisegn0  5837  dmsnsnsn  5952  sucprc  6141  dffv3  6534  fconst5  6835  1stval  7547  2ndval  7548  ecexr  8144  snfi  8442  domunsn  8514  snnen2o  8553  hashrabrsn  13581  hashrabsn01  13582  hashrabsn1  13583  elprchashprn2  13605  hashsn01  13625  hash2pwpr  13680  efgrelexlema  18602  usgr1v  26721  1conngr  27660  frgr1v  27742  n0lplig  27951  unidifsnne  29985  eldm3  32606  opelco3  32627  fvsingle  32991  unisnif  32996  funpartlem  33013  bj-sngltag  33919  bj-restsnid  33996  bj-snmoore  34024  wopprc  39131  sn1dom  39396  uneqsn  39877