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

Theorem supeq1d 7926
Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
supeq1d.1
Assertion
Ref Expression
supeq1d

Proof of Theorem supeq1d
StepHypRef Expression
1 supeq1d.1 . 2
2 supeq1 7925 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  supcsup 7920
This theorem is referenced by:  supminf  11198  rpnnen1  11242  reexALT  11243  limsupval  13297  limsupgval  13299  rpnnen  13960  gcdval  14146  gcdass  14183  odzval  14318  pcval  14368  pceulem  14369  pceu  14370  pczpre  14371  pcdiv  14376  pcneg  14397  prmreclem1  14434  prmreclem5  14438  ramval  14526  ramz  14543  prdsval  14852  prdsdsval  14875  prdsdsval2  14881  prdsdsval3  14882  imasval  14908  imasdsval  14912  gexval  16598  ressprdsds  20874  xpsdsval  20884  tmsxpsval  21041  nmofval  21221  nmoval  21222  metdsval  21351  bndth  21458  lebnumlem1  21461  lebnumlem3  21463  ovolval  21885  elovolmr  21887  ovolctb  21901  ovoliunlem3  21915  ovolshftlem1  21920  ovolshft  21922  voliunlem3  21962  voliun  21964  volsup  21966  ioorf  21982  mbfinf  22072  mbflimsup  22073  itg1climres  22121  itg2val  22135  itg2monolem1  22157  itg2i1fseq  22162  itg2cnlem1  22168  mdegfval  22460  mdegfvalOLD  22461  mdegval  22462  mdegvalOLD  22463  mdeg0  22470  mdegvsca  22476  mdegpropd  22484  deg1val  22496  deg1valOLD  22497  deg1mul3  22516  ig1pval  22573  dgrval  22625  coe11  22650  elqaalem1  22715  elqaalem2  22716  elqaalem3  22717  elqaa  22718  nmoofval  25677  nmooval  25678  nmoo0  25706  nmopval  26775  nmfnval  26795  esumval  28057  esum0  28060  esumsn  28072  esumfsupre  28077  omsval  28264  omsfval  28265  ballotlemi  28439  erdszelem3  28637  erdsze  28646  elwlim  29379  ee7.2aOLD  29926  supadd  30042  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnc  30069  pellfundval  30816  aomclem8  31007  dgraaval  31093  lcmval  31198  lcmass  31218  fourierdlem31  31920  fourierdlem79  31968  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem105  31994  fourierdlem108  31997  fourierdlem110  31999
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-ral 2812  df-rex 2813  df-rab 2816  df-uni 4250  df-sup 7921
  Copyright terms: Public domain W3C validator