Theorem supeq1d 9337

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 9336	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1541  supcsup 9331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-uni 4859  df-sup 9333

This theorem is referenced by:  supadd  12097  supminf  12835  rpnnen1lem6  12882  rpnnen1  12883  limsupval  15383  limsupgval  15385  gcdval  16409  gcdass  16460  pcval  16758  pceulem  16759  pceu  16760  pczpre  16761  pcdiv  16766  pcneg  16788  prmreclem1  16830  prmreclem5  16834  ramz  16939  prdsval  17361  prdsdsval  17384  prdsdsval2  17390  prdsdsval3  17391  ressprdsds  24287  xpsdsval  24297  tmsxpsval  24454  bndth  24885  elovolmr  25405  ovolctb  25419  ovoliunlem3  25433  ovolshftlem1  25438  voliunlem3  25481  voliun  25483  volsup  25485  ioorf  25502  mbfinf  25594  itg1climres  25643  itg2val  25657  itg2monolem1  25679  itg2i1fseq  25684  itg2cnlem1  25690  mdegfval  25995  mdegval  25996  mdeg0  26003  mdegvsca  26009  mdegpropd  26017  deg1val  26029  deg1mul3  26049  dgrval  26161  coe11  26186  nmoofval  30744  nmooval  30745  nmoo0  30773  nmopval  31838  nmfnval  31858  ressdeg1  33536  esumval  34080  esum0  34083  esumsnf  34098  esumfsupre  34105  esumsup  34123  erdszelem3  35258  erdsze  35267  elwlim  35886  ee7.2aOLD  36526  poimirlem32  37713  ovoliunnfl  37723  voliunnfl  37725  volsupnfl  37726  itg2addnc  37735  aomclem8  43179  infnsuprnmpt  45372  supsubc  45477  supxrmnf2  45556  supminfxr  45587  limsupval3  45815  limsupresre  45819  limsuplesup  45822  limsupresico  45823  limsupvaluz  45831  limsupvaluzmpt  45840  limsupvaluz2  45861  supcnvlimsup  45863  supcnvlimsupmpt  45864  limsuplt2  45876  liminfval  45882  limsupge  45884  liminfval5  45888  limsupresxr  45889  liminfresxr  45890  liminfresico  45894  limsup10ex  45896  liminflelimsuplem  45898  fourierdlem79  46308  fourierdlem96  46325  fourierdlem97  46326  fourierdlem98  46327  fourierdlem99  46328  fourierdlem105  46334  fourierdlem108  46337  fourierdlem110  46339  sge0val  46489  sge0z  46498  sge0revalmpt  46501  sge0sn  46502  sge0tsms  46503  sge0f1o  46505  sge0sup  46514  sge0resplit  46529  meaiuninclem  46603  smfsuplem2  46935  smfsup  46937  smfsupmpt  46938  smflimsuplem1  46943  smflimsuplem2  46944  smflimsuplem4  46946  smflimsuplem5  46947  smflimsuplem7  46949  smflimsup  46951