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

Theorem snprc 4683
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 4607 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21exbii 1851 . . 3 (∃𝑥 𝑥 ∈ {𝐴} ↔ ∃𝑥 𝑥 = 𝐴)
3 neq0 4310 . . 3 (¬ {𝐴} = ∅ ↔ ∃𝑥 𝑥 ∈ {𝐴})
4 isset 3461 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
52, 3, 43bitr4i 303 . 2 (¬ {𝐴} = ∅ ↔ 𝐴 ∈ V)
65con1bii 357 1 𝐴 ∈ V ↔ {𝐴} = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1542  wex 1782  wcel 2107  Vcvv 3448  c0 4287  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-nul 4288  df-sn 4592
This theorem is referenced by:  snnzb  4684  rmosn  4685  rabsnif  4689  prprc1  4731  prprc  4733  preqsnd  4821  unisn2  5274  eqsnuniex  5321  snexALT  5343  snex  5393  posn  5722  frsn  5724  relsnb  5763  relimasn  6041  elimasni  6048  inisegn0  6055  dmsnsnsn  6177  predprc  6297  sucprc  6398  dffv3  6843  fconst5  7160  ordsuci  7748  1stval  7928  2ndval  7929  ecexr  8660  snfi  8995  domunsn  9078  snnen2oOLD  9178  hashrabrsn  14279  hashrabsn01  14280  hashrabsn1  14281  elprchashprn2  14303  hashsn01  14323  hash2pwpr  14382  snsymgefmndeq  19183  efgrelexlema  19538  usgr1v  28246  1conngr  29180  frgr1v  29257  n0lplig  29467  unidifsnne  31505  eldm3  34373  opelco3  34388  fvsingle  34534  unisnif  34539  funpartlem  34556  bj-sngltag  35483  bj-snex  35535  bj-restsnid  35587  bj-snmooreb  35614  wopprc  41383  safesnsupfidom1o  41763  sn1dom  41872  uneqsn  42371  vsn  46970  mofsn2  46985
  Copyright terms: Public domain W3C validator