Theorem supeq1d 9394

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

Syntax hints:   → wi 4   = wceq 1563  supcsup 9388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-ss 3924  df-uni 4868  df-sup 9390

This theorem is referenced by:  supadd  12171  supminf  12947  rpnnen1lem6  12994  rpnnen1  12995  limsupval  15513  limsupgval  15515  gcdval  16542  gcdass  16593  pcval  16892  pceulem  16893  pceu  16894  pczpre  16895  pcdiv  16900  pcneg  16922  prmreclem1  16964  prmreclem5  16968  ramz  17073  prdsval  17496  prdsdsval  17519  prdsdsval2  17525  prdsdsval3  17526  ressprdsds  24485  xpsdsval  24495  tmsxpsval  24652  bndth  25074  elovolmr  25592  ovolctb  25606  ovoliunlem3  25620  ovolshftlem1  25625  voliunlem3  25668  voliun  25670  volsup  25672  ioorf  25689  mbfinf  25781  itg1climres  25830  itg2val  25844  itg2monolem1  25866  itg2i1fseq  25871  itg2cnlem1  25877  mdegfval  26176  mdegval  26177  mdeg0  26184  mdegvsca  26190  mdegpropd  26198  deg1val  26210  deg1mul3  26230  dgrval  26342  coe11  26367  nmoofval  31019  nmooval  31020  nmoo0  31048  nmopval  32113  nmfnval  32133  ressdeg1  33768  esumval  34348  esum0  34351  esumsnf  34366  esumfsupre  34373  esumsup  34391  erdszelem3  35551  erdsze  35560  elwlim  36179  ee7.2aOLD  36829  poimirlem32  38158  ovoliunnfl  38168  voliunnfl  38170  volsupnfl  38171  itg2addnc  38180  aomclem8  43645  infnsuprnmpt  45824  supsubc  45928  supxrmnf2  46006  supminfxr  46037  limsupval3  46265  limsupresre  46269  limsuplesup  46272  limsupresico  46273  limsupvaluz  46281  limsupvaluzmpt  46290  limsupvaluz2  46311  supcnvlimsup  46313  supcnvlimsupmpt  46314  limsuplt2  46326  liminfval  46332  limsupge  46334  liminfval5  46338  limsupresxr  46339  liminfresxr  46340  liminfresico  46344  limsup10ex  46346  liminflelimsuplem  46348  fourierdlem79  46758  fourierdlem96  46775  fourierdlem97  46776  fourierdlem98  46777  fourierdlem99  46778  fourierdlem105  46784  fourierdlem108  46787  fourierdlem110  46789  sge0val  46939  sge0z  46948  sge0revalmpt  46951  sge0sn  46952  sge0tsms  46953  sge0f1o  46955  sge0sup  46964  sge0resplit  46979  meaiuninclem  47053  smfsuplem2  47385  smfsup  47387  smfsupmpt  47388  smflimsuplem1  47393  smflimsuplem2  47394  smflimsuplem4  47396  smflimsuplem5  47397  smflimsuplem7  47399  smflimsup  47401