MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snprc Structured version   Visualization version   GIF version

Theorem snprc 4408
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.
StepHypRef Expression
1 velsn 4350 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1943 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 4094 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3360 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
52, 3, 43bitr4i 294 . 2 (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
65con1bii 347 1 𝐴 ∈ V ↔ {𝐴} = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197   = wceq 1652  wex 1874  wcel 2155  Vcvv 3350  c0 4079  {csn 4334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-nul 4080  df-sn 4335
This theorem is referenced by:  snnzb  4409  rabsnif  4413  prprc1  4455  prprc  4457  preqsnd  4543  unisn2  4955  snexALT  5018  snex  5064  posn  5357  frsn  5359  relimasn  5670  elimasni  5674  inisegn0  5679  dmsnsnsn  5797  sucprc  5983  dffv3  6371  fconst5  6664  1stval  7368  2ndval  7369  ecexr  7952  snfi  8245  domunsn  8317  snnen2o  8356  hashrabrsn  13363  hashrabsn01  13364  hashrabsn1  13365  elprchashprn2  13385  hashsn01  13405  hash2pwpr  13459  efgrelexlema  18428  usgr1v  26427  1conngr  27430  frgr1v  27509  n0lplig  27729  eldm3  32028  opelco3  32053  fvsingle  32403  unisnif  32408  funpartlem  32425  bj-sngltag  33330  bj-restsnid  33400  bj-snmoore  33428  wopprc  38206  uneqsn  38927
  Copyright terms: Public domain W3C validator