Theorem supeq1d 9356

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

Syntax hints:   → wi 4   = wceq 1547  supcsup 9350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-ss 3907  df-uni 4846  df-sup 9352

This theorem is referenced by:  supadd  12122  supminf  12883  rpnnen1lem6  12930  rpnnen1  12931  limsupval  15434  limsupgval  15436  gcdval  16463  gcdass  16514  pcval  16813  pceulem  16814  pceu  16815  pczpre  16816  pcdiv  16821  pcneg  16843  prmreclem1  16885  prmreclem5  16889  ramz  16994  prdsval  17416  prdsdsval  17439  prdsdsval2  17445  prdsdsval3  17446  ressprdsds  24361  xpsdsval  24371  tmsxpsval  24528  bndth  24950  elovolmr  25468  ovolctb  25482  ovoliunlem3  25496  ovolshftlem1  25501  voliunlem3  25544  voliun  25546  volsup  25548  ioorf  25565  mbfinf  25657  itg1climres  25706  itg2val  25720  itg2monolem1  25742  itg2i1fseq  25747  itg2cnlem1  25753  mdegfval  26052  mdegval  26053  mdeg0  26060  mdegvsca  26066  mdegpropd  26074  deg1val  26086  deg1mul3  26106  dgrval  26218  coe11  26243  nmoofval  30858  nmooval  30859  nmoo0  30887  nmopval  31952  nmfnval  31972  ressdeg1  33656  esumval  34237  esum0  34240  esumsnf  34255  esumfsupre  34262  esumsup  34280  erdszelem3  35428  erdsze  35437  elwlim  36056  ee7.2aOLD  36696  poimirlem32  38026  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  itg2addnc  38048  aomclem8  43513  infnsuprnmpt  45701  supsubc  45805  supxrmnf2  45883  supminfxr  45914  limsupval3  46142  limsupresre  46146  limsuplesup  46149  limsupresico  46150  limsupvaluz  46158  limsupvaluzmpt  46167  limsupvaluz2  46188  supcnvlimsup  46190  supcnvlimsupmpt  46191  limsuplt2  46203  liminfval  46209  limsupge  46211  liminfval5  46215  limsupresxr  46216  liminfresxr  46217  liminfresico  46221  limsup10ex  46223  liminflelimsuplem  46225  fourierdlem79  46635  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem105  46661  fourierdlem108  46664  fourierdlem110  46666  sge0val  46816  sge0z  46825  sge0revalmpt  46828  sge0sn  46829  sge0tsms  46830  sge0f1o  46832  sge0sup  46841  sge0resplit  46856  meaiuninclem  46930  smfsuplem2  47262  smfsup  47264  smfsupmpt  47265  smflimsuplem1  47270  smflimsuplem2  47271  smflimsuplem4  47273  smflimsuplem5  47274  smflimsuplem7  47276  smflimsup  47278