Theorem snprc 4681

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 4603	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3		neq0 4302	. . 3 ⊢ (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4		isset 3467	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
6	5	con1bii 359	1 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3453  ∅c0 4282  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-nul 4283  df-sn 4588

This theorem is used by:  snnzb  4682  rmosn  4683  rabsnif  4687  prprc1  4729  prprc  4731  preqsnd  4822  unisn2  5273  eqsnuniex  5330  snexALT  5352  snexOLD  5411  posn  5745  frsn  5747  relsnb  5787  relimasn  6085  elimasni  6091  inisegn0  6098  dmsnsnsn  6220  predprc  6340  sucprc  6440  dffv3  6878  fconst5  7209  ordsuci  7811  1stval  7992  2ndval  7993  ecexr  8705  snfi  9054  domunsn  9129  hashrabrsn  14440  hashrabsn01  14441  hashrabsn1  14442  elprchashprn2  14464  hashsn01  14485  hash2pwpr  14545  snsymgefmndeq  19528  efgrelexlema  19882  usgr1v  29724  1conngr  30682  frgr1v  30759  n0lplig  30972  unidifsnne  33019  eldm3  36348  opelco3  36362  fvsingle  36505  unisnif  36510  funpartlem  36529  bj-sngltag  37735  bj-snex  37787  bj-restsnid  37845  bj-snmooreb  37872  wopprc  43879  safesnsupfidom1o  44265  sn1dom  44374  uneqsn  44873  vsn  49748  mofsn2  49781