Theorem supeq1d 9416

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  supcsup 9410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-ss 3925  df-uni 4878  df-sup 9412

This theorem is used by:  supadd  12201  supminf  12977  rpnnen1lem6  13024  rpnnen1  13025  limsupval  15551  limsupgval  15553  gcdval  16579  gcdass  16630  pcval  16929  pceulem  16930  pceu  16931  pczpre  16932  pcdiv  16937  pcneg  16959  prmreclem1  17001  prmreclem5  17005  ramz  17110  prdsval  17533  prdsdsval  17556  prdsdsval2  17562  prdsdsval3  17563  ressprdsds  24565  xpsdsval  24575  tmsxpsval  24732  bndth  25154  elovolmr  25672  ovolctb  25686  ovoliunlem3  25700  ovolshftlem1  25705  voliunlem3  25748  voliun  25750  volsup  25752  ioorf  25769  mbfinf  25861  itg1climres  25910  itg2val  25924  itg2monolem1  25946  itg2i1fseq  25951  itg2cnlem1  25957  mdegfval  26256  mdegval  26257  mdeg0  26264  mdegvsca  26270  mdegpropd  26278  deg1val  26290  deg1mul3  26310  dgrval  26422  coe11  26447  nmoofval  31151  nmooval  31152  nmoo0  31180  nmopval  32245  nmfnval  32265  ressdeg1  33887  esumval  34467  esum0  34470  esumsnf  34485  esumfsupre  34492  esumsup  34510  erdszelem3  35706  erdsze  35715  elwlim  36334  ee7.2aOLD  37013  poimirlem32  38344  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  itg2addnc  38366  aomclem8  43829  infnsuprnmpt  46006  supsubc  46110  supxrmnf2  46188  supminfxr  46219  limsupval3  46447  limsupresre  46451  limsuplesup  46454  limsupresico  46455  limsupvaluz  46463  limsupvaluzmpt  46472  limsupvaluz2  46493  supcnvlimsup  46495  supcnvlimsupmpt  46496  limsuplt2  46508  liminfval  46514  limsupge  46516  liminfval5  46520  limsupresxr  46521  liminfresxr  46522  liminfresico  46526  limsup10ex  46528  liminflelimsuplem  46530  fourierdlem79  46940  fourierdlem96  46957  fourierdlem97  46958  fourierdlem98  46959  fourierdlem99  46960  fourierdlem105  46966  fourierdlem108  46969  fourierdlem110  46971  sge0val  47121  sge0z  47130  sge0revalmpt  47133  sge0sn  47134  sge0tsms  47135  sge0f1o  47137  sge0sup  47146  sge0resplit  47161  meaiuninclem  47235  smfsuplem2  47567  smfsup  47569  smfsupmpt  47570  smflimsuplem1  47575  smflimsuplem2  47576  smflimsuplem4  47578  smflimsuplem5  47579  smflimsuplem7  47581  smflimsup  47583