Theorem supeq1d 9404

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

Syntax hints:   → wi 4   = wceq 1540  supcsup 9398

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-ss 3934  df-uni 4875  df-sup 9400

This theorem is referenced by:  supadd  12158  supminf  12901  rpnnen1lem6  12948  rpnnen1  12949  limsupval  15447  limsupgval  15449  gcdval  16473  gcdass  16524  pcval  16822  pceulem  16823  pceu  16824  pczpre  16825  pcdiv  16830  pcneg  16852  prmreclem1  16894  prmreclem5  16898  ramz  17003  prdsval  17425  prdsdsval  17448  prdsdsval2  17454  prdsdsval3  17455  ressprdsds  24266  xpsdsval  24276  tmsxpsval  24433  bndth  24864  elovolmr  25384  ovolctb  25398  ovoliunlem3  25412  ovolshftlem1  25417  voliunlem3  25460  voliun  25462  volsup  25464  ioorf  25481  mbfinf  25573  itg1climres  25622  itg2val  25636  itg2monolem1  25658  itg2i1fseq  25663  itg2cnlem1  25669  mdegfval  25974  mdegval  25975  mdeg0  25982  mdegvsca  25988  mdegpropd  25996  deg1val  26008  deg1mul3  26028  dgrval  26140  coe11  26165  nmoofval  30698  nmooval  30699  nmoo0  30727  nmopval  31792  nmfnval  31812  ressdeg1  33542  esumval  34043  esum0  34046  esumsnf  34061  esumfsupre  34068  esumsup  34086  erdszelem3  35187  erdsze  35196  elwlim  35818  ee7.2aOLD  36456  poimirlem32  37653  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnc  37675  aomclem8  43057  infnsuprnmpt  45251  supsubc  45356  supxrmnf2  45436  supminfxr  45467  limsupval3  45697  limsupresre  45701  limsuplesup  45704  limsupresico  45705  limsupvaluz  45713  limsupvaluzmpt  45722  limsupvaluz2  45743  supcnvlimsup  45745  supcnvlimsupmpt  45746  limsuplt2  45758  liminfval  45764  limsupge  45766  liminfval5  45770  limsupresxr  45771  liminfresxr  45772  liminfresico  45776  limsup10ex  45778  liminflelimsuplem  45780  fourierdlem79  46190  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem105  46216  fourierdlem108  46219  fourierdlem110  46221  sge0val  46371  sge0z  46380  sge0revalmpt  46383  sge0sn  46384  sge0tsms  46385  sge0f1o  46387  sge0sup  46396  sge0resplit  46411  meaiuninclem  46485  smfsuplem2  46817  smfsup  46819  smfsupmpt  46820  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem4  46828  smflimsuplem5  46829  smflimsuplem7  46831  smflimsup  46833