Theorem supeq1d 9441

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

Syntax hints:   → wi 4   = wceq 1542  supcsup 9435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-sup 9437

This theorem is referenced by:  supadd  12182  supminf  12919  rpnnen1lem6  12966  rpnnen1  12967  limsupval  15418  limsupgval  15420  gcdval  16437  gcdass  16489  pcval  16777  pceulem  16778  pceu  16779  pczpre  16780  pcdiv  16785  pcneg  16807  prmreclem1  16849  prmreclem5  16853  ramz  16958  prdsval  17401  prdsdsval  17424  prdsdsval2  17430  prdsdsval3  17431  ressprdsds  23877  xpsdsval  23887  tmsxpsval  24047  bndth  24474  elovolmr  24993  ovolctb  25007  ovoliunlem3  25021  ovolshftlem1  25026  voliunlem3  25069  voliun  25071  volsup  25073  ioorf  25090  mbfinf  25182  itg1climres  25232  itg2val  25246  itg2monolem1  25268  itg2i1fseq  25273  itg2cnlem1  25279  mdegfval  25580  mdegval  25581  mdeg0  25588  mdegvsca  25594  mdegpropd  25602  deg1val  25614  deg1mul3  25633  dgrval  25742  coe11  25767  nmoofval  30015  nmooval  30016  nmoo0  30044  nmopval  31109  nmfnval  31129  ressdeg1  32651  esumval  33044  esum0  33047  esumsnf  33062  esumfsupre  33069  esumsup  33087  erdszelem3  34184  erdsze  34193  elwlim  34795  ee7.2aOLD  35346  poimirlem32  36520  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnc  36542  aomclem8  41803  infnsuprnmpt  43954  supsubc  44063  supxrmnf2  44143  supminfxr  44174  limsupval3  44408  limsupresre  44412  limsuplesup  44415  limsupresico  44416  limsupvaluz  44424  limsupvaluzmpt  44433  limsupvaluz2  44454  supcnvlimsup  44456  supcnvlimsupmpt  44457  limsuplt2  44469  liminfval  44475  limsupge  44477  liminfval5  44481  limsupresxr  44482  liminfresxr  44483  liminfresico  44487  limsup10ex  44489  liminflelimsuplem  44491  fourierdlem79  44901  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem105  44927  fourierdlem108  44930  fourierdlem110  44932  sge0val  45082  sge0z  45091  sge0revalmpt  45094  sge0sn  45095  sge0tsms  45096  sge0f1o  45098  sge0sup  45107  sge0resplit  45122  meaiuninclem  45196  smfsuplem2  45528  smfsup  45530  smfsupmpt  45531  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem4  45539  smflimsuplem5  45540  smflimsuplem7  45542  smflimsup  45544