Theorem supeq1d 9419

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  supcsup 9413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-sup 9415

This theorem is used by:  supadd  12210  supminf  12987  rpnnen1lem6  13034  rpnnen1  13035  limsupval  15563  limsupgval  15565  gcdval  16590  gcdass  16641  pcval  16940  pceulem  16941  pceu  16942  pczpre  16943  pcdiv  16948  pcneg  16970  prmreclem1  17012  prmreclem5  17016  ramz  17121  prdsval  17544  prdsdsval  17567  prdsdsval2  17573  prdsdsval3  17574  ressprdsds  24598  xpsdsval  24608  tmsxpsval  24765  bndth  25187  elovolmr  25705  ovolctb  25719  ovoliunlem3  25733  ovolshftlem1  25738  voliunlem3  25781  voliun  25783  volsup  25785  ioorf  25802  mbfinf  25894  itg1climres  25943  itg2val  25957  itg2monolem1  25979  itg2i1fseq  25984  itg2cnlem1  25990  mdegfval  26289  mdegval  26290  mdeg0  26297  mdegvsca  26303  mdegpropd  26311  deg1val  26323  deg1mul3  26343  dgrval  26455  coe11  26480  nmoofval  31229  nmooval  31230  nmoo0  31258  nmopval  32323  nmfnval  32343  ressdeg1  33963  esumval  34543  esum0  34546  esumsnf  34561  esumfsupre  34568  esumsup  34586  erdszelem3  35759  erdsze  35768  elwlim  36387  ee7.2aOLD  37067  poimirlem32  38388  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  itg2addnc  38410  aomclem8  43889  infnsuprnmpt  46066  supsubc  46170  supxrmnf2  46248  supminfxr  46279  limsupval3  46507  limsupresre  46511  limsuplesup  46514  limsupresico  46515  limsupvaluz  46523  limsupvaluzmpt  46532  limsupvaluz2  46553  supcnvlimsup  46555  supcnvlimsupmpt  46556  limsuplt2  46568  liminfval  46574  limsupge  46576  liminfval5  46580  limsupresxr  46581  liminfresxr  46582  liminfresico  46586  limsup10ex  46588  liminflelimsuplem  46590  fourierdlem79  47000  fourierdlem96  47017  fourierdlem97  47018  fourierdlem98  47019  fourierdlem99  47020  fourierdlem105  47026  fourierdlem108  47029  fourierdlem110  47031  sge0val  47181  sge0z  47190  sge0revalmpt  47193  sge0sn  47194  sge0tsms  47195  sge0f1o  47197  sge0sup  47206  sge0resplit  47221  meaiuninclem  47295  smfsuplem2  47627  smfsup  47629  smfsupmpt  47630  smflimsuplem1  47635  smflimsuplem2  47636  smflimsuplem4  47638  smflimsuplem5  47639  smflimsuplem7  47641  smflimsup  47643