Theorem supeq1d 8352

Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1d.1	|- ( ph -> B = C )

Assertion

Ref	Expression
supeq1d	|- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )

Proof of Theorem supeq1d

Step	Hyp	Ref	Expression
1		supeq1d.1	. 2 |- ( ph -> B = C )
2		supeq1 8351	. 2 |- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
3	1, 2	syl 17	1 |- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )

Syntax hints:   -> wi 4   = wceq 1483   supcsup 8346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-uni 4437  df-sup 8348

This theorem is referenced by:  supadd  10991  supminf  11775  rpnnen1lem6  11819  rpnnen1  11820  rpnnen1OLD  11825  limsupval  14205  limsupgval  14207  gcdval  15218  gcdass  15264  pcval  15549  pceulem  15550  pceu  15551  pczpre  15552  pcdiv  15557  pcneg  15578  prmreclem1  15620  prmreclem5  15624  ramz  15729  prdsval  16115  prdsdsval  16138  prdsdsval2  16144  prdsdsval3  16145  ressprdsds  22176  xpsdsval  22186  tmsxpsval  22343  bndth  22757  elovolmr  23244  ovolctb  23258  ovoliunlem3  23272  ovolshftlem1  23277  voliunlem3  23320  voliun  23322  volsup  23324  ioorf  23341  mbfinf  23432  itg1climres  23481  itg2val  23495  itg2monolem1  23517  itg2i1fseq  23522  itg2cnlem1  23528  mdegfval  23822  mdegval  23823  mdeg0  23830  mdegvsca  23836  mdegpropd  23844  deg1val  23856  deg1mul3  23875  dgrval  23984  coe11  24009  nmoofval  27617  nmooval  27618  nmoo0  27646  nmopval  28715  nmfnval  28735  esumval  30108  esum0  30111  esumsnf  30126  esumfsupre  30133  esumsup  30151  erdszelem3  31175  erdsze  31184  elwlim  31769  elwlimOLD  31770  ee7.2aOLD  32460  poimirlem32  33441  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnc  33464  aomclem8  37631  infnsuprnmpt  39465  supsubc  39569  supxrmnf2  39660  supminfxr  39694  limsupval3  39924  limsupresre  39928  limsuplesup  39931  limsupresico  39932  limsupvaluz  39940  limsupvaluzmpt  39949  limsupvaluz2  39970  supcnvlimsup  39972  supcnvlimsupmpt  39973  limsuplt2  39985  liminfval  39991  limsupge  39993  liminfval5  39997  limsupresxr  39998  liminfresxr  39999  liminfresico  40003  limsup10ex  40005  liminflelimsuplem  40007  fourierdlem79  40402  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem105  40428  fourierdlem108  40431  fourierdlem110  40433  sge0val  40583  sge0z  40592  sge0revalmpt  40595  sge0sn  40596  sge0tsms  40597  sge0f1o  40599  sge0sup  40608  sge0resplit  40623  meaiuninclem  40697  smfsuplem2  41018  smfsup  41020  smfsupmpt  41021  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem4  41029  smflimsuplem5  41030  smflimsuplem7  41032  smflimsup  41034