Theorem supeq1d 9359

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

Syntax hints:   → wi 4   = wceq 1542  supcsup 9353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-ss 3906  df-uni 4851  df-sup 9355

This theorem is referenced by:  supadd  12124  supminf  12885  rpnnen1lem6  12932  rpnnen1  12933  limsupval  15436  limsupgval  15438  gcdval  16465  gcdass  16516  pcval  16815  pceulem  16816  pceu  16817  pczpre  16818  pcdiv  16823  pcneg  16845  prmreclem1  16887  prmreclem5  16891  ramz  16996  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  ressprdsds  24336  xpsdsval  24346  tmsxpsval  24503  bndth  24925  elovolmr  25443  ovolctb  25457  ovoliunlem3  25471  ovolshftlem1  25476  voliunlem3  25519  voliun  25521  volsup  25523  ioorf  25540  mbfinf  25632  itg1climres  25681  itg2val  25695  itg2monolem1  25717  itg2i1fseq  25722  itg2cnlem1  25728  mdegfval  26027  mdegval  26028  mdeg0  26035  mdegvsca  26041  mdegpropd  26049  deg1val  26061  deg1mul3  26081  dgrval  26193  coe11  26218  nmoofval  30833  nmooval  30834  nmoo0  30862  nmopval  31927  nmfnval  31947  ressdeg1  33626  esumval  34190  esum0  34193  esumsnf  34208  esumfsupre  34215  esumsup  34233  erdszelem3  35375  erdsze  35384  elwlim  36003  ee7.2aOLD  36643  poimirlem32  37973  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnc  37995  aomclem8  43489  infnsuprnmpt  45679  supsubc  45783  supxrmnf2  45861  supminfxr  45892  limsupval3  46120  limsupresre  46124  limsuplesup  46127  limsupresico  46128  limsupvaluz  46136  limsupvaluzmpt  46145  limsupvaluz2  46166  supcnvlimsup  46168  supcnvlimsupmpt  46169  limsuplt2  46181  liminfval  46187  limsupge  46189  liminfval5  46193  limsupresxr  46194  liminfresxr  46195  liminfresico  46199  limsup10ex  46201  liminflelimsuplem  46203  fourierdlem79  46613  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem105  46639  fourierdlem108  46642  fourierdlem110  46644  sge0val  46794  sge0z  46803  sge0revalmpt  46806  sge0sn  46807  sge0tsms  46808  sge0f1o  46810  sge0sup  46819  sge0resplit  46834  meaiuninclem  46908  smfsuplem2  47240  smfsup  47242  smfsupmpt  47243  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256