Theorem supeq1d 9443

Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1d.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
supeq1d	⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Proof of Theorem supeq1d

Step	Hyp	Ref	Expression
1		supeq1d.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
2		supeq1 9442	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1539  supcsup 9437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-sup 9439

This theorem is referenced by:  supadd  12186  supminf  12923  rpnnen1lem6  12970  rpnnen1  12971  limsupval  15422  limsupgval  15424  gcdval  16441  gcdass  16493  pcval  16781  pceulem  16782  pceu  16783  pczpre  16784  pcdiv  16789  pcneg  16811  prmreclem1  16853  prmreclem5  16857  ramz  16962  prdsval  17405  prdsdsval  17428  prdsdsval2  17434  prdsdsval3  17435  ressprdsds  24097  xpsdsval  24107  tmsxpsval  24267  bndth  24704  elovolmr  25225  ovolctb  25239  ovoliunlem3  25253  ovolshftlem1  25258  voliunlem3  25301  voliun  25303  volsup  25305  ioorf  25322  mbfinf  25414  itg1climres  25464  itg2val  25478  itg2monolem1  25500  itg2i1fseq  25505  itg2cnlem1  25511  mdegfval  25815  mdegval  25816  mdeg0  25823  mdegvsca  25829  mdegpropd  25837  deg1val  25849  deg1mul3  25868  dgrval  25977  coe11  26002  nmoofval  30282  nmooval  30283  nmoo0  30311  nmopval  31376  nmfnval  31396  ressdeg1  32925  esumval  33342  esum0  33345  esumsnf  33360  esumfsupre  33367  esumsup  33385  erdszelem3  34482  erdsze  34491  elwlim  35099  ee7.2aOLD  35649  poimirlem32  36823  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  itg2addnc  36845  aomclem8  42105  infnsuprnmpt  44252  supsubc  44361  supxrmnf2  44441  supminfxr  44472  limsupval3  44706  limsupresre  44710  limsuplesup  44713  limsupresico  44714  limsupvaluz  44722  limsupvaluzmpt  44731  limsupvaluz2  44752  supcnvlimsup  44754  supcnvlimsupmpt  44755  limsuplt2  44767  liminfval  44773  limsupge  44775  liminfval5  44779  limsupresxr  44780  liminfresxr  44781  liminfresico  44785  limsup10ex  44787  liminflelimsuplem  44789  fourierdlem79  45199  fourierdlem96  45216  fourierdlem97  45217  fourierdlem98  45218  fourierdlem99  45219  fourierdlem105  45225  fourierdlem108  45228  fourierdlem110  45230  sge0val  45380  sge0z  45389  sge0revalmpt  45392  sge0sn  45393  sge0tsms  45394  sge0f1o  45396  sge0sup  45405  sge0resplit  45420  meaiuninclem  45494  smfsuplem2  45826  smfsup  45828  smfsupmpt  45829  smflimsuplem1  45834  smflimsuplem2  45835  smflimsuplem4  45837  smflimsuplem5  45838  smflimsuplem7  45840  smflimsup  45842