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

Theorem supeq1d 7895
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 7894 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2syl 16 1  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374   supcsup 7889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-uni 4239  df-sup 7890
This theorem is referenced by:  supminf  11158  rpnnen1  11202  reexALT  11203  limsupval  13246  limsupgval  13248  rpnnen  13810  gcdval  13994  gcdass  14031  odzval  14166  pcval  14216  pceulem  14217  pceu  14218  pczpre  14219  pcdiv  14224  pcneg  14245  prmreclem1  14282  prmreclem5  14286  ramval  14374  ramz  14391  prdsval  14699  prdsdsval  14722  prdsdsval2  14728  prdsdsval3  14729  imasval  14755  imasdsval  14759  gexval  16387  ressprdsds  20602  xpsdsval  20612  tmsxpsval  20769  nmofval  20949  nmoval  20950  metdsval  21079  bndth  21186  lebnumlem1  21189  lebnumlem3  21191  ovolval  21613  elovolmr  21615  ovolctb  21629  ovoliunlem3  21643  ovolshftlem1  21648  ovolshft  21650  voliunlem3  21690  voliun  21692  volsup  21694  ioorf  21710  mbfinf  21800  mbflimsup  21801  itg1climres  21849  itg2val  21863  itg2monolem1  21885  itg2i1fseq  21890  itg2cnlem1  21896  mdegfval  22188  mdegfvalOLD  22189  mdegval  22190  mdegvalOLD  22191  mdeg0  22198  mdegvsca  22204  mdegpropd  22212  deg1val  22224  deg1valOLD  22225  deg1mul3  22244  ig1pval  22301  dgrval  22353  coe11  22377  elqaalem1  22442  elqaalem2  22443  elqaalem3  22444  elqaa  22445  nmoofval  25339  nmooval  25340  nmoo0  25368  nmopval  26437  nmfnval  26457  esumval  27683  esum0  27686  esumsn  27698  esumfsupre  27703  omsval  27890  omsfval  27891  ballotlemi  28065  erdszelem3  28263  erdsze  28272  elwlim  28942  ee7.2aOLD  29489  supadd  29605  ovoliunnfl  29620  voliunnfl  29622  volsupnfl  29623  itg2addnc  29633  pellfundval  30407  aomclem8  30600  dgraaval  30687  fourierdlem31  31393  fourierdlem79  31441  fourierdlem96  31458  fourierdlem97  31459  fourierdlem98  31460  fourierdlem99  31461  fourierdlem105  31467  fourierdlem108  31470
  Copyright terms: Public domain W3C validator