MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supeq1d Structured version   Visualization version   GIF version

Theorem supeq1d 9214
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
StepHypRef Expression
1 supeq1d.1 . 2 (𝜑𝐵 = 𝐶)
2 supeq1 9213 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  supcsup 9208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-sup 9210
This theorem is referenced by:  supadd  11952  supminf  12684  rpnnen1lem6  12731  rpnnen1  12732  limsupval  15192  limsupgval  15194  gcdval  16212  gcdass  16264  pcval  16554  pceulem  16555  pceu  16556  pczpre  16557  pcdiv  16562  pcneg  16584  prmreclem1  16626  prmreclem5  16630  ramz  16735  prdsval  17175  prdsdsval  17198  prdsdsval2  17204  prdsdsval3  17205  ressprdsds  23533  xpsdsval  23543  tmsxpsval  23703  bndth  24130  elovolmr  24649  ovolctb  24663  ovoliunlem3  24677  ovolshftlem1  24682  voliunlem3  24725  voliun  24727  volsup  24729  ioorf  24746  mbfinf  24838  itg1climres  24888  itg2val  24902  itg2monolem1  24924  itg2i1fseq  24929  itg2cnlem1  24935  mdegfval  25236  mdegval  25237  mdeg0  25244  mdegvsca  25250  mdegpropd  25258  deg1val  25270  deg1mul3  25289  dgrval  25398  coe11  25423  nmoofval  29133  nmooval  29134  nmoo0  29162  nmopval  30227  nmfnval  30247  esumval  32023  esum0  32026  esumsnf  32041  esumfsupre  32048  esumsup  32066  erdszelem3  33164  erdsze  33173  elwlim  33826  ee7.2aOLD  34659  poimirlem32  35818  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnc  35840  aomclem8  40893  infnsuprnmpt  42803  supsubc  42899  supxrmnf2  42980  supminfxr  43011  limsupval3  43240  limsupresre  43244  limsuplesup  43247  limsupresico  43248  limsupvaluz  43256  limsupvaluzmpt  43265  limsupvaluz2  43286  supcnvlimsup  43288  supcnvlimsupmpt  43289  limsuplt2  43301  liminfval  43307  limsupge  43309  liminfval5  43313  limsupresxr  43314  liminfresxr  43315  liminfresico  43319  limsup10ex  43321  liminflelimsuplem  43323  fourierdlem79  43733  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem105  43759  fourierdlem108  43762  fourierdlem110  43764  sge0val  43911  sge0z  43920  sge0revalmpt  43923  sge0sn  43924  sge0tsms  43925  sge0f1o  43927  sge0sup  43936  sge0resplit  43951  meaiuninclem  44025  smfsuplem2  44356  smfsup  44358  smfsupmpt  44359  smflimsuplem1  44364  smflimsuplem2  44365  smflimsuplem4  44367  smflimsuplem5  44368  smflimsuplem7  44370  smflimsup  44372
  Copyright terms: Public domain W3C validator