Theorem supeq1d 9397

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

Syntax hints:   → wi 4   = wceq 1540  supcsup 9391

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-ss 3931  df-uni 4872  df-sup 9393

This theorem is referenced by:  supadd  12151  supminf  12894  rpnnen1lem6  12941  rpnnen1  12942  limsupval  15440  limsupgval  15442  gcdval  16466  gcdass  16517  pcval  16815  pceulem  16816  pceu  16817  pczpre  16818  pcdiv  16823  pcneg  16845  prmreclem1  16887  prmreclem5  16891  ramz  16996  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  ressprdsds  24259  xpsdsval  24269  tmsxpsval  24426  bndth  24857  elovolmr  25377  ovolctb  25391  ovoliunlem3  25405  ovolshftlem1  25410  voliunlem3  25453  voliun  25455  volsup  25457  ioorf  25474  mbfinf  25566  itg1climres  25615  itg2val  25629  itg2monolem1  25651  itg2i1fseq  25656  itg2cnlem1  25662  mdegfval  25967  mdegval  25968  mdeg0  25975  mdegvsca  25981  mdegpropd  25989  deg1val  26001  deg1mul3  26021  dgrval  26133  coe11  26158  nmoofval  30691  nmooval  30692  nmoo0  30720  nmopval  31785  nmfnval  31805  ressdeg1  33535  esumval  34036  esum0  34039  esumsnf  34054  esumfsupre  34061  esumsup  34079  erdszelem3  35180  erdsze  35189  elwlim  35811  ee7.2aOLD  36449  poimirlem32  37646  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnc  37668  aomclem8  43050  infnsuprnmpt  45244  supsubc  45349  supxrmnf2  45429  supminfxr  45460  limsupval3  45690  limsupresre  45694  limsuplesup  45697  limsupresico  45698  limsupvaluz  45706  limsupvaluzmpt  45715  limsupvaluz2  45736  supcnvlimsup  45738  supcnvlimsupmpt  45739  limsuplt2  45751  liminfval  45757  limsupge  45759  liminfval5  45763  limsupresxr  45764  liminfresxr  45765  liminfresico  45769  limsup10ex  45771  liminflelimsuplem  45773  fourierdlem79  46183  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem105  46209  fourierdlem108  46212  fourierdlem110  46214  sge0val  46364  sge0z  46373  sge0revalmpt  46376  sge0sn  46377  sge0tsms  46378  sge0f1o  46380  sge0sup  46389  sge0resplit  46404  meaiuninclem  46478  smfsuplem2  46810  smfsup  46812  smfsupmpt  46813  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  smflimsup  46826