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

Theorem elsnc2 3669
 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 3668 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wb 176   wceq 1623   wcel 1684  cvv 2788  csn 3640 This theorem is referenced by:  fparlem1  6218  fparlem2  6219  el1o  6498  fin1a2lem11  8036  fin1a2lem12  8037  elnn0  9967  elfzp1  10836  fsumss  12198  elhoma  13864  islpidl  15998  zrhrhmb  16465  rest0  16900  divstgphaus  17805  taylfval  19738  elch0  21833  atoml2i  22963  climrec  27729  dibopelvalN  31333  dibopelval2  31335 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
 Copyright terms: Public domain W3C validator