Theorem supeq1d 9486

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

Syntax hints:   → wi 4   = wceq 1540  supcsup 9480

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-uni 4908  df-sup 9482

This theorem is referenced by:  supadd  12236  supminf  12977  rpnnen1lem6  13024  rpnnen1  13025  limsupval  15510  limsupgval  15512  gcdval  16533  gcdass  16584  pcval  16882  pceulem  16883  pceu  16884  pczpre  16885  pcdiv  16890  pcneg  16912  prmreclem1  16954  prmreclem5  16958  ramz  17063  prdsval  17500  prdsdsval  17523  prdsdsval2  17529  prdsdsval3  17530  ressprdsds  24381  xpsdsval  24391  tmsxpsval  24551  bndth  24990  elovolmr  25511  ovolctb  25525  ovoliunlem3  25539  ovolshftlem1  25544  voliunlem3  25587  voliun  25589  volsup  25591  ioorf  25608  mbfinf  25700  itg1climres  25749  itg2val  25763  itg2monolem1  25785  itg2i1fseq  25790  itg2cnlem1  25796  mdegfval  26101  mdegval  26102  mdeg0  26109  mdegvsca  26115  mdegpropd  26123  deg1val  26135  deg1mul3  26155  dgrval  26267  coe11  26292  nmoofval  30781  nmooval  30782  nmoo0  30810  nmopval  31875  nmfnval  31895  ressdeg1  33591  esumval  34047  esum0  34050  esumsnf  34065  esumfsupre  34072  esumsup  34090  erdszelem3  35198  erdsze  35207  elwlim  35824  ee7.2aOLD  36462  poimirlem32  37659  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnc  37681  aomclem8  43073  infnsuprnmpt  45257  supsubc  45364  supxrmnf2  45444  supminfxr  45475  limsupval3  45707  limsupresre  45711  limsuplesup  45714  limsupresico  45715  limsupvaluz  45723  limsupvaluzmpt  45732  limsupvaluz2  45753  supcnvlimsup  45755  supcnvlimsupmpt  45756  limsuplt2  45768  liminfval  45774  limsupge  45776  liminfval5  45780  limsupresxr  45781  liminfresxr  45782  liminfresico  45786  limsup10ex  45788  liminflelimsuplem  45790  fourierdlem79  46200  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem105  46226  fourierdlem108  46229  fourierdlem110  46231  sge0val  46381  sge0z  46390  sge0revalmpt  46393  sge0sn  46394  sge0tsms  46395  sge0f1o  46397  sge0sup  46406  sge0resplit  46421  meaiuninclem  46495  smfsuplem2  46827  smfsup  46829  smfsupmpt  46830  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem4  46838  smflimsuplem5  46839  smflimsuplem7  46841  smflimsup  46843