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

Theorem supeq1d 7969
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 7968 . 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 1437   supcsup 7963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-rab 2780  df-uni 4220  df-sup 7965
This theorem is referenced by:  supadd  10582  supminf  11257  supminfOLD  11258  rpnnen1  11302  reexALT  11303  limsupval  13530  limsupvalOLD  13531  limsupgval  13533  rpnnen  14278  gcdval  14469  gcdass  14512  lcmvalOLD  14555  lcmslefacOLD  14585  lcmfvalOLD  14594  odzvalOLD  14741  pcval  14793  pceulem  14794  pceu  14795  pczpre  14796  pcdiv  14801  pcneg  14822  prmreclem1  14859  prmreclem5  14863  ramvalOLD  14960  ramz  14982  prmgaplcmlem1OLD  15011  prmordvdslcmsOLDOLD  15020  prmorlelcmsOLDOLD  15021  prdsval  15352  prdsdsval  15375  prdsdsval2  15381  prdsdsval3  15382  imasvalOLD  15411  imasdsvalOLD  15427  gexvalOLD  17228  ressprdsds  21384  xpsdsval  21394  tmsxpsval  21551  nmofvalOLD  21736  nmovalOLD  21737  metdsvalOLD  21877  bndth  21984  lebnumlem1OLD  21990  lebnumlem3OLD  21992  ovolvalOLD  22425  elovolmr  22427  ovolctb  22441  ovoliunlem3  22455  ovolshftlem1  22460  voliunlem3  22503  voliun  22505  volsup  22507  ioorf  22523  ioorfOLD  22528  mbfinf  22619  mbfinfOLD  22620  mbflimsupOLD  22622  itg1climres  22670  itg2val  22684  itg2monolem1  22706  itg2i1fseq  22711  itg2cnlem1  22717  mdegfval  23009  mdegval  23010  mdeg0  23017  mdegvsca  23023  mdegpropd  23031  deg1val  23043  deg1mul3  23062  ig1pvalOLD  23128  dgrval  23180  coe11  23205  elqaalem1OLD  23273  elqaalem2OLD  23274  elqaalem3OLD  23275  nmoofval  26401  nmooval  26402  nmoo0  26430  nmopval  27507  nmfnval  27527  esumval  28875  esum0  28878  esumsnf  28893  esumfsupre  28900  esumsup  28918  omsvalOLD  29129  omsfvalOLD  29130  ballotlemiOLD  29379  erdszelem3  29924  erdsze  29933  elwlim  30513  ee7.2aOLD  31126  poimirlem32  31936  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  itg2addnc  31960  pellfundvalOLD  35698  aomclem8  35889  dgraavalOLD  35976  supsubc  37530  fourierdlem31OLD  37941  fourierdlem79  37989  fourierdlem96  38006  fourierdlem97  38007  fourierdlem98  38008  fourierdlem99  38009  fourierdlem105  38015  fourierdlem108  38018  fourierdlem110  38020  sge0val  38116  sge0z  38125  sge0revalmpt  38128  sge0sn  38129  sge0tsms  38130  sge0f1o  38132  sge0sup  38141  sge0resplit  38156
  Copyright terms: Public domain W3C validator