Theorem supeq1d 9361

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

Syntax hints:   → wi 4   = wceq 1542  supcsup 9355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-ss 3920  df-uni 4866  df-sup 9357

This theorem is referenced by:  supadd  12122  supminf  12860  rpnnen1lem6  12907  rpnnen1  12908  limsupval  15409  limsupgval  15411  gcdval  16435  gcdass  16486  pcval  16784  pceulem  16785  pceu  16786  pczpre  16787  pcdiv  16792  pcneg  16814  prmreclem1  16856  prmreclem5  16860  ramz  16965  prdsval  17387  prdsdsval  17410  prdsdsval2  17416  prdsdsval3  17417  ressprdsds  24327  xpsdsval  24337  tmsxpsval  24494  bndth  24925  elovolmr  25445  ovolctb  25459  ovoliunlem3  25473  ovolshftlem1  25478  voliunlem3  25521  voliun  25523  volsup  25525  ioorf  25542  mbfinf  25634  itg1climres  25683  itg2val  25697  itg2monolem1  25719  itg2i1fseq  25724  itg2cnlem1  25730  mdegfval  26035  mdegval  26036  mdeg0  26043  mdegvsca  26049  mdegpropd  26057  deg1val  26069  deg1mul3  26089  dgrval  26201  coe11  26226  nmoofval  30849  nmooval  30850  nmoo0  30878  nmopval  31943  nmfnval  31963  ressdeg1  33658  esumval  34223  esum0  34226  esumsnf  34241  esumfsupre  34248  esumsup  34266  erdszelem3  35406  erdsze  35415  elwlim  36034  ee7.2aOLD  36674  poimirlem32  37900  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  itg2addnc  37922  aomclem8  43415  infnsuprnmpt  45605  supsubc  45709  supxrmnf2  45788  supminfxr  45819  limsupval3  46047  limsupresre  46051  limsuplesup  46054  limsupresico  46055  limsupvaluz  46063  limsupvaluzmpt  46072  limsupvaluz2  46093  supcnvlimsup  46095  supcnvlimsupmpt  46096  limsuplt2  46108  liminfval  46114  limsupge  46116  liminfval5  46120  limsupresxr  46121  liminfresxr  46122  liminfresico  46126  limsup10ex  46128  liminflelimsuplem  46130  fourierdlem79  46540  fourierdlem96  46557  fourierdlem97  46558  fourierdlem98  46559  fourierdlem99  46560  fourierdlem105  46566  fourierdlem108  46569  fourierdlem110  46571  sge0val  46721  sge0z  46730  sge0revalmpt  46733  sge0sn  46734  sge0tsms  46735  sge0f1o  46737  sge0sup  46746  sge0resplit  46761  meaiuninclem  46835  smfsuplem2  47167  smfsup  47169  smfsupmpt  47170  smflimsuplem1  47175  smflimsuplem2  47176  smflimsuplem4  47178  smflimsuplem5  47179  smflimsuplem7  47181  smflimsup  47183