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

Theorem supeq1d 7941
Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
supeq1d.1  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
supeq1d  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)

Proof of Theorem supeq1d
StepHypRef Expression
1 supeq1d.1 . 2  |-  ( ph  ->  B  =  C )
2 supeq1 7940 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2syl 17 1  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407   supcsup 7936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ral 2761  df-rex 2762  df-rab 2765  df-uni 4194  df-sup 7937
This theorem is referenced by:  supminf  11216  rpnnen1  11260  reexALT  11261  limsupval  13448  limsupgval  13450  rpnnen  14171  gcdval  14357  gcdass  14394  odzval  14529  pcval  14579  pceulem  14580  pceu  14581  pczpre  14582  pcdiv  14587  pcneg  14608  prmreclem1  14645  prmreclem5  14649  ramval  14737  ramz  14754  prdsval  15071  prdsdsval  15094  prdsdsval2  15100  prdsdsval3  15101  imasval  15127  imasdsval  15131  gexval  16924  ressprdsds  21168  xpsdsval  21178  tmsxpsval  21335  nmofval  21515  nmoval  21516  metdsval  21645  bndth  21752  lebnumlem1  21755  lebnumlem3  21757  ovolval  22179  elovolmr  22181  ovolctb  22195  ovoliunlem3  22209  ovolshftlem1  22214  ovolshft  22216  voliunlem3  22256  voliun  22258  volsup  22260  ioorf  22276  mbfinf  22366  mbflimsup  22367  itg1climres  22415  itg2val  22429  itg2monolem1  22451  itg2i1fseq  22456  itg2cnlem1  22462  mdegfval  22754  mdegfvalOLD  22755  mdegval  22756  mdegvalOLD  22757  mdeg0  22764  mdegvsca  22770  mdegpropd  22778  deg1val  22790  deg1valOLD  22791  deg1mul3  22810  ig1pval  22867  dgrval  22919  coe11  22944  elqaalem1  23009  elqaalem2  23010  elqaalem3  23011  elqaa  23012  nmoofval  26104  nmooval  26105  nmoo0  26133  nmopval  27201  nmfnval  27221  esumval  28506  esum0  28509  esumsnf  28524  esumfsupre  28531  esumsup  28549  omsval  28754  omsfval  28755  ballotlemi  28958  erdszelem3  29503  erdsze  29512  elwlim  30092  ee7.2aOLD  30706  supadd  31427  ovoliunnfl  31441  voliunnfl  31443  volsupnfl  31444  itg2addnc  31455  pellfundval  35190  aomclem8  35382  dgraaval  35470  lcmval  36059  lcmass  36079  fourierdlem31  37301  fourierdlem79  37349  fourierdlem96  37366  fourierdlem97  37367  fourierdlem98  37368  fourierdlem99  37369  fourierdlem105  37375  fourierdlem108  37378  fourierdlem110  37380
  Copyright terms: Public domain W3C validator