Theorem snprc 4655

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 4585	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4311	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3508	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 305	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496  ∅c0 4293  {csn 4569

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-nul 4294  df-sn 4570

This theorem is referenced by:  snnzb  4656  rmosn  4657  rabsnif  4661  prprc1  4703  prprc  4705  preqsnd  4791  unisn2  5218  snexALT  5286  snex  5334  posn  5639  frsn  5641  relsnb  5677  relimasn  5954  elimasni  5958  inisegn0  5963  dmsnsnsn  6079  sucprc  6268  dffv3  6668  fconst5  6970  1stval  7693  2ndval  7694  ecexr  8296  snfi  8596  domunsn  8669  snnen2o  8709  hashrabrsn  13736  hashrabsn01  13737  hashrabsn1  13738  elprchashprn2  13760  hashsn01  13780  hash2pwpr  13837  snsymgefmndeq  18525  efgrelexlema  18877  usgr1v  27040  1conngr  27975  frgr1v  28052  n0lplig  28262  unidifsnne  30298  eldm3  32999  opelco3  33020  fvsingle  33383  unisnif  33388  funpartlem  33405  bj-sngltag  34297  bj-restsnid  34380  bj-snmooreb  34408  wopprc  39634  sn1dom  39899  uneqsn  40380