Theorem supeq1d 9407

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

Syntax hints:   → wi 4   = wceq 1570  supcsup 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-ss 3923  df-uni 4874  df-sup 9403

This theorem is referenced by:  supadd  12184  supminf  12960  rpnnen1lem6  13007  rpnnen1  13008  limsupval  15527  limsupgval  15529  gcdval  16555  gcdass  16606  pcval  16905  pceulem  16906  pceu  16907  pczpre  16908  pcdiv  16913  pcneg  16935  prmreclem1  16977  prmreclem5  16981  ramz  17086  prdsval  17509  prdsdsval  17532  prdsdsval2  17538  prdsdsval3  17539  ressprdsds  24509  xpsdsval  24519  tmsxpsval  24676  bndth  25098  elovolmr  25616  ovolctb  25630  ovoliunlem3  25644  ovolshftlem1  25649  voliunlem3  25692  voliun  25694  volsup  25696  ioorf  25713  mbfinf  25805  itg1climres  25854  itg2val  25868  itg2monolem1  25890  itg2i1fseq  25895  itg2cnlem1  25901  mdegfval  26200  mdegval  26201  mdeg0  26208  mdegvsca  26214  mdegpropd  26222  deg1val  26234  deg1mul3  26254  dgrval  26366  coe11  26391  nmoofval  31095  nmooval  31096  nmoo0  31124  nmopval  32189  nmfnval  32209  ressdeg1  33837  esumval  34417  esum0  34420  esumsnf  34435  esumfsupre  34442  esumsup  34460  erdszelem3  35666  erdsze  35675  elwlim  36294  ee7.2aOLD  36953  poimirlem32  38284  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  itg2addnc  38306  aomclem8  43771  infnsuprnmpt  45948  supsubc  46052  supxrmnf2  46130  supminfxr  46161  limsupval3  46389  limsupresre  46393  limsuplesup  46396  limsupresico  46397  limsupvaluz  46405  limsupvaluzmpt  46414  limsupvaluz2  46435  supcnvlimsup  46437  supcnvlimsupmpt  46438  limsuplt2  46450  liminfval  46456  limsupge  46458  liminfval5  46462  limsupresxr  46463  liminfresxr  46464  liminfresico  46468  limsup10ex  46470  liminflelimsuplem  46472  fourierdlem79  46882  fourierdlem96  46899  fourierdlem97  46900  fourierdlem98  46901  fourierdlem99  46902  fourierdlem105  46908  fourierdlem108  46911  fourierdlem110  46913  sge0val  47063  sge0z  47072  sge0revalmpt  47075  sge0sn  47076  sge0tsms  47077  sge0f1o  47079  sge0sup  47088  sge0resplit  47103  meaiuninclem  47177  smfsuplem2  47509  smfsup  47511  smfsupmpt  47512  smflimsuplem1  47517  smflimsuplem2  47518  smflimsuplem4  47520  smflimsuplem5  47521  smflimsuplem7  47523  smflimsup  47525