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

Theorem supeq1d 7694
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 7693 . 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 1369   supcsup 7688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-uni 4090  df-sup 7689
This theorem is referenced by:  supminf  10940  rpnnen1  10982  reexALT  10983  limsupval  12950  limsupgval  12952  rpnnen  13507  gcdval  13690  gcdass  13727  odzval  13861  pcval  13909  pceulem  13910  pceu  13911  pczpre  13912  pcdiv  13917  pcneg  13938  prmreclem1  13975  prmreclem5  13979  ramval  14067  ramz  14084  prdsval  14391  prdsdsval  14414  prdsdsval2  14420  prdsdsval3  14421  imasval  14447  imasdsval  14451  gexval  16075  ressprdsds  19944  xpsdsval  19954  tmsxpsval  20111  nmofval  20291  nmoval  20292  metdsval  20421  bndth  20528  lebnumlem1  20531  lebnumlem3  20533  ovolval  20955  elovolmr  20957  ovolctb  20971  ovoliunlem3  20985  ovolshftlem1  20990  ovolshft  20992  voliunlem3  21031  voliun  21033  volsup  21035  ioorf  21051  mbfinf  21141  mbflimsup  21142  itg1climres  21190  itg2val  21204  itg2monolem1  21226  itg2i1fseq  21231  itg2cnlem1  21237  mdegfval  21529  mdegfvalOLD  21530  mdegval  21531  mdegvalOLD  21532  mdeg0  21539  mdegvsca  21545  mdegpropd  21553  deg1val  21565  deg1valOLD  21566  deg1mul3  21585  ig1pval  21642  dgrval  21694  coe11  21718  elqaalem1  21783  elqaalem2  21784  elqaalem3  21785  elqaa  21786  nmoofval  24160  nmooval  24161  nmoo0  24189  nmopval  25258  nmfnval  25278  esumval  26498  esum0  26501  esumsn  26513  esumfsupre  26518  omsval  26706  omsfval  26707  ballotlemi  26881  erdszelem3  27079  erdsze  27088  elwlim  27758  ee7.2aOLD  28305  supadd  28415  ovoliunnfl  28430  voliunnfl  28432  volsupnfl  28433  itg2addnc  28443  pellfundval  29218  aomclem8  29411  dgraaval  29498
  Copyright terms: Public domain W3C validator