Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsnc2 Structured version   Unicode version

Theorem elsnc2 4002
 Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that , rather than , be a set. (Contributed by NM, 12-Jun-1994.)
Hypothesis
Ref Expression
elsnc2.1
Assertion
Ref Expression
elsnc2

Proof of Theorem elsnc2
StepHypRef Expression
1 elsnc2.1 . 2
2 elsnc2g 4001 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wceq 1405   wcel 1842  cvv 3058  csn 3971 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380 This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-sn 3972 This theorem is referenced by:  fparlem1  6883  fparlem2  6884  el1o  7185  fin1a2lem11  8821  fin1a2lem12  8822  elnn0  10837  elfzp1  11783  fsumss  13694  fprodss  13905  elhoma  15633  islpidl  18212  zrhrhmb  18846  rest0  19961  qustgphaus  20911  taylfval  23044  elch0  26572  atoml2i  27701  bj-eltag  31087  dibopelvalN  34143  dibopelval2  34145  climrec  36958
 Copyright terms: Public domain W3C validator