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

Theorem elsnc 4053
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
Hypothesis
Ref Expression
elsnc.1
Assertion
Ref Expression
elsnc

Proof of Theorem elsnc
StepHypRef Expression
1 elsnc.1 . 2
2 elsncg 4052 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818   cvv 3109  {csn 4029
This theorem is referenced by:  sneqr  4197  opthwiener  4754  snsn0non  5001  opthprc  5052  dmsnn0  5478  dmsnopg  5484  cnvcnvsn  5490  sniota  5583  funconstss  6005  fniniseg  6008  fniniseg2  6010  fsn  6069  fconstfv  6133  eusvobj2  6289  fnse  6917  fisn  7907  mapfienOLD  8159  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  ttukeylem7  8916  opelreal  9528  seqid3  12151  seqz  12155  1exp  12195  hashf1lem2  12505  imasaddfnlem  14925  0subg  16226  0nsg  16246  sylow2alem2  16638  gsumval3OLD  16908  gsumval3  16911  gsumzaddlem  16934  gsumzaddlemOLD  16936  kerf1hrm  17392  lsssn0  17594  r0cld  20239  alexsubALTlem2  20548  tgphaus  20615  isusp  20764  i1f1lem  22096  ig1pcl  22576  plyco0  22589  plyeq0lem  22607  plycj  22674  wilthlem2  23343  dchrfi  23530  hsn0elch  26166  h1de2ctlem  26473  atomli  27301  kerunit  27813  qqhval2lem  27962  qqhf  27967  qqhre  27998  eulerpartlemb  28307  subfacp1lem6  28629  wfrlem14  29356  ellimits  29560  itg2addnclem2  30067  ftc1anclem3  30092  0idl  30422  keridl  30429  smprngopr  30449  isdmn3  30471  pw2f1ocnv  30979  fprodn0f  31594  usgra2pthlem1  32353  initoid  32611  termoid  32612  lindslinindsimp1  33058  bnj149  33933  bj-0nel1  34509  ellkr  34814  diblss  36897  dihmeetlem4preN  37033  dihmeetlem13N  37046  snhesn  37809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030
  Copyright terms: Public domain W3C validator