Theorem supeq1d 8763

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

Syntax hints:   → wi 4   = wceq 1525  supcsup 8757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-rex 3113  df-rab 3116  df-uni 4752  df-sup 8759

This theorem is referenced by:  supadd  11463  supminf  12188  rpnnen1lem6  12235  rpnnen1  12236  limsupval  14669  limsupgval  14671  gcdval  15682  gcdass  15728  pcval  16014  pceulem  16015  pceu  16016  pczpre  16017  pcdiv  16022  pcneg  16043  prmreclem1  16085  prmreclem5  16089  ramz  16194  prdsval  16561  prdsdsval  16584  prdsdsval2  16590  prdsdsval3  16591  ressprdsds  22668  xpsdsval  22678  tmsxpsval  22835  bndth  23249  elovolmr  23764  ovolctb  23778  ovoliunlem3  23792  ovolshftlem1  23797  voliunlem3  23840  voliun  23842  volsup  23844  ioorf  23861  mbfinf  23953  itg1climres  24002  itg2val  24016  itg2monolem1  24038  itg2i1fseq  24043  itg2cnlem1  24049  mdegfval  24343  mdegval  24344  mdeg0  24351  mdegvsca  24357  mdegpropd  24365  deg1val  24377  deg1mul3  24396  dgrval  24505  coe11  24530  nmoofval  28226  nmooval  28227  nmoo0  28255  nmopval  29320  nmfnval  29340  esumval  30918  esum0  30921  esumsnf  30936  esumfsupre  30943  esumsup  30961  erdszelem3  32050  erdsze  32059  elwlim  32721  ee7.2aOLD  33420  poimirlem32  34476  ovoliunnfl  34486  voliunnfl  34488  volsupnfl  34489  itg2addnc  34498  aomclem8  39167  infnsuprnmpt  41084  supsubc  41183  supxrmnf2  41270  supminfxr  41303  limsupval3  41536  limsupresre  41540  limsuplesup  41543  limsupresico  41544  limsupvaluz  41552  limsupvaluzmpt  41561  limsupvaluz2  41582  supcnvlimsup  41584  supcnvlimsupmpt  41585  limsuplt2  41597  liminfval  41603  limsupge  41605  liminfval5  41609  limsupresxr  41610  liminfresxr  41611  liminfresico  41615  limsup10ex  41617  liminflelimsuplem  41619  fourierdlem79  42034  fourierdlem96  42051  fourierdlem97  42052  fourierdlem98  42053  fourierdlem99  42054  fourierdlem105  42060  fourierdlem108  42063  fourierdlem110  42065  sge0val  42212  sge0z  42221  sge0revalmpt  42224  sge0sn  42225  sge0tsms  42226  sge0f1o  42228  sge0sup  42237  sge0resplit  42252  meaiuninclem  42326  smfsuplem2  42650  smfsup  42652  smfsupmpt  42653  smflimsuplem1  42658  smflimsuplem2  42659  smflimsuplem4  42661  smflimsuplem5  42662  smflimsuplem7  42664  smflimsup  42666