Theorem supeq1d 9463

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

Syntax hints:   → wi 4   = wceq 1540  supcsup 9457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-ss 3948  df-uni 4889  df-sup 9459

This theorem is referenced by:  supadd  12215  supminf  12956  rpnnen1lem6  13003  rpnnen1  13004  limsupval  15495  limsupgval  15497  gcdval  16520  gcdass  16571  pcval  16869  pceulem  16870  pceu  16871  pczpre  16872  pcdiv  16877  pcneg  16899  prmreclem1  16941  prmreclem5  16945  ramz  17050  prdsval  17474  prdsdsval  17497  prdsdsval2  17503  prdsdsval3  17504  ressprdsds  24315  xpsdsval  24325  tmsxpsval  24482  bndth  24913  elovolmr  25434  ovolctb  25448  ovoliunlem3  25462  ovolshftlem1  25467  voliunlem3  25510  voliun  25512  volsup  25514  ioorf  25531  mbfinf  25623  itg1climres  25672  itg2val  25686  itg2monolem1  25708  itg2i1fseq  25713  itg2cnlem1  25719  mdegfval  26024  mdegval  26025  mdeg0  26032  mdegvsca  26038  mdegpropd  26046  deg1val  26058  deg1mul3  26078  dgrval  26190  coe11  26215  nmoofval  30748  nmooval  30749  nmoo0  30777  nmopval  31842  nmfnval  31862  ressdeg1  33584  esumval  34082  esum0  34085  esumsnf  34100  esumfsupre  34107  esumsup  34125  erdszelem3  35220  erdsze  35229  elwlim  35846  ee7.2aOLD  36484  poimirlem32  37681  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  itg2addnc  37703  aomclem8  43052  infnsuprnmpt  45241  supsubc  45347  supxrmnf2  45427  supminfxr  45458  limsupval3  45688  limsupresre  45692  limsuplesup  45695  limsupresico  45696  limsupvaluz  45704  limsupvaluzmpt  45713  limsupvaluz2  45734  supcnvlimsup  45736  supcnvlimsupmpt  45737  limsuplt2  45749  liminfval  45755  limsupge  45757  liminfval5  45761  limsupresxr  45762  liminfresxr  45763  liminfresico  45767  limsup10ex  45769  liminflelimsuplem  45771  fourierdlem79  46181  fourierdlem96  46198  fourierdlem97  46199  fourierdlem98  46200  fourierdlem99  46201  fourierdlem105  46207  fourierdlem108  46210  fourierdlem110  46212  sge0val  46362  sge0z  46371  sge0revalmpt  46374  sge0sn  46375  sge0tsms  46376  sge0f1o  46378  sge0sup  46387  sge0resplit  46402  meaiuninclem  46476  smfsuplem2  46808  smfsup  46810  smfsupmpt  46811  smflimsuplem1  46816  smflimsuplem2  46817  smflimsuplem4  46819  smflimsuplem5  46820  smflimsuplem7  46822  smflimsup  46824