Theorem supeq1d 9468

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-uni 4871  df-sup 9464

This theorem is used by:  supadd  12315  supminf  13092  rpnnen1lem6  13140  rpnnen1  13141  limsupval  15673  limsupgval  15675  gcdval  16698  gcdass  16752  pcval  17054  pceulem  17055  pceu  17056  pczpre  17057  pcdiv  17062  pcneg  17084  prmreclem1  17126  prmreclem5  17130  ramz  17235  prdsval  17658  prdsdsval  17681  prdsdsval2  17687  prdsdsval3  17688  ressprdsds  24723  xpsdsval  24733  tmsxpsval  24890  bndth  25312  elovolmr  25830  ovolctb  25844  ovoliunlem3  25858  ovolshftlem1  25863  voliunlem3  25906  voliun  25908  volsup  25910  ioorf  25927  mbfinf  26019  itg1climres  26068  itg2val  26082  itg2monolem1  26104  itg2i1fseq  26109  itg2cnlem1  26115  mdegfval  26413  mdegval  26414  mdeg0  26421  mdegvsca  26427  mdegpropd  26435  deg1val  26447  deg1mul3  26467  dgrval  26580  coe11  26605  nmoofval  31397  nmooval  31398  nmoo0  31426  nmopval  32491  nmfnval  32511  ressdeg1  34181  esumval  34761  esum0  34764  esumsnf  34779  esumfsupre  34786  esumsup  34804  erdszelem3  36138  erdsze  36147  elwlim  36776  ee7.2aOLD  37440  poimirlem32  38775  ovoliunnfl  38785  voliunnfl  38787  volsupnfl  38788  itg2addnc  38797  aomclem8  44267  infnsuprnmpt  46477  supsubc  46580  supxrmnf2  46658  supminfxr  46689  limsupval3  46917  limsupresre  46921  limsuplesup  46924  limsupresico  46925  limsupvaluz  46933  limsupvaluzmpt  46942  limsupvaluz2  46963  supcnvlimsup  46965  supcnvlimsupmpt  46966  limsuplt2  46978  liminfval  46984  limsupge  46986  liminfval5  46990  limsupresxr  46991  liminfresxr  46992  liminfresico  46996  limsup10ex  46998  liminflelimsuplem  47000  fourierdlem79  47410  fourierdlem96  47427  fourierdlem97  47428  fourierdlem98  47429  fourierdlem99  47430  fourierdlem105  47436  fourierdlem108  47439  fourierdlem110  47441  sge0val  47591  sge0z  47600  sge0revalmpt  47603  sge0sn  47604  sge0tsms  47605  sge0f1o  47607  sge0sup  47616  sge0resplit  47631  meaiuninclem  47705  smfsuplem2  48037  smfsup  48039  smfsupmpt  48040  smflimsuplem1  48045  smflimsuplem2  48046  smflimsuplem4  48048  smflimsuplem5  48049  smflimsuplem7  48051  smflimsup  48053