Theorem supeq1d 9389

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

Syntax hints:   → wi 4   = wceq 1559  supcsup 9383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-ss 3921  df-uni 4865  df-sup 9385

This theorem is referenced by:  supadd  12157  supminf  12933  rpnnen1lem6  12980  rpnnen1  12981  limsupval  15484  limsupgval  15486  gcdval  16513  gcdass  16564  pcval  16863  pceulem  16864  pceu  16865  pczpre  16866  pcdiv  16871  pcneg  16893  prmreclem1  16935  prmreclem5  16939  ramz  17044  prdsval  17467  prdsdsval  17490  prdsdsval2  17496  prdsdsval3  17497  ressprdsds  24411  xpsdsval  24421  tmsxpsval  24578  bndth  25000  elovolmr  25518  ovolctb  25532  ovoliunlem3  25546  ovolshftlem1  25551  voliunlem3  25594  voliun  25596  volsup  25598  ioorf  25615  mbfinf  25707  itg1climres  25756  itg2val  25770  itg2monolem1  25792  itg2i1fseq  25797  itg2cnlem1  25803  mdegfval  26102  mdegval  26103  mdeg0  26110  mdegvsca  26116  mdegpropd  26124  deg1val  26136  deg1mul3  26156  dgrval  26268  coe11  26293  nmoofval  30911  nmooval  30912  nmoo0  30940  nmopval  32005  nmfnval  32025  ressdeg1  33723  esumval  34304  esum0  34307  esumsnf  34322  esumfsupre  34329  esumsup  34347  erdszelem3  35507  erdsze  35516  elwlim  36135  ee7.2aOLD  36785  poimirlem32  38115  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  itg2addnc  38137  aomclem8  43602  infnsuprnmpt  45789  supsubc  45893  supxrmnf2  45971  supminfxr  46002  limsupval3  46230  limsupresre  46234  limsuplesup  46237  limsupresico  46238  limsupvaluz  46246  limsupvaluzmpt  46255  limsupvaluz2  46276  supcnvlimsup  46278  supcnvlimsupmpt  46279  limsuplt2  46291  liminfval  46297  limsupge  46299  liminfval5  46303  limsupresxr  46304  liminfresxr  46305  liminfresico  46309  limsup10ex  46311  liminflelimsuplem  46313  fourierdlem79  46723  fourierdlem96  46740  fourierdlem97  46741  fourierdlem98  46742  fourierdlem99  46743  fourierdlem105  46749  fourierdlem108  46752  fourierdlem110  46754  sge0val  46904  sge0z  46913  sge0revalmpt  46916  sge0sn  46917  sge0tsms  46918  sge0f1o  46920  sge0sup  46929  sge0resplit  46944  meaiuninclem  47018  smfsuplem2  47350  smfsup  47352  smfsupmpt  47353  smflimsuplem1  47358  smflimsuplem2  47359  smflimsuplem4  47361  smflimsuplem5  47362  smflimsuplem7  47364  smflimsup  47366