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

Theorem supeq1d 8561
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 8560 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  supcsup 8555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-uni 4597  df-sup 8557
This theorem is referenced by:  supadd  11247  supminf  11979  rpnnen1lem6  12023  rpnnen1  12024  limsupval  14493  limsupgval  14495  gcdval  15502  gcdass  15548  pcval  15831  pceulem  15832  pceu  15833  pczpre  15834  pcdiv  15839  pcneg  15860  prmreclem1  15902  prmreclem5  15906  ramz  16011  prdsval  16384  prdsdsval  16407  prdsdsval2  16413  prdsdsval3  16414  ressprdsds  22458  xpsdsval  22468  tmsxpsval  22625  bndth  23039  elovolmr  23537  ovolctb  23551  ovoliunlem3  23565  ovolshftlem1  23570  voliunlem3  23613  voliun  23615  volsup  23617  ioorf  23634  mbfinf  23726  itg1climres  23775  itg2val  23789  itg2monolem1  23811  itg2i1fseq  23816  itg2cnlem1  23822  mdegfval  24116  mdegval  24117  mdeg0  24124  mdegvsca  24130  mdegpropd  24138  deg1val  24150  deg1mul3  24169  dgrval  24278  coe11  24303  nmoofval  28076  nmooval  28077  nmoo0  28105  nmopval  29174  nmfnval  29194  esumval  30558  esum0  30561  esumsnf  30576  esumfsupre  30583  esumsup  30601  erdszelem3  31626  erdsze  31635  elwlim  32215  ee7.2aOLD  32902  poimirlem32  33868  ovoliunnfl  33878  voliunnfl  33880  volsupnfl  33881  itg2addnc  33890  aomclem8  38311  infnsuprnmpt  40109  supsubc  40210  supxrmnf2  40300  supminfxr  40334  limsupval3  40565  limsupresre  40569  limsuplesup  40572  limsupresico  40573  limsupvaluz  40581  limsupvaluzmpt  40590  limsupvaluz2  40611  supcnvlimsup  40613  supcnvlimsupmpt  40614  limsuplt2  40626  liminfval  40632  limsupge  40634  liminfval5  40638  limsupresxr  40639  liminfresxr  40640  liminfresico  40644  limsup10ex  40646  liminflelimsuplem  40648  fourierdlem79  41042  fourierdlem96  41059  fourierdlem97  41060  fourierdlem98  41061  fourierdlem99  41062  fourierdlem105  41068  fourierdlem108  41071  fourierdlem110  41073  sge0val  41223  sge0z  41232  sge0revalmpt  41235  sge0sn  41236  sge0tsms  41237  sge0f1o  41239  sge0sup  41248  sge0resplit  41263  meaiuninclem  41337  smfsuplem2  41661  smfsup  41663  smfsupmpt  41664  smflimsuplem1  41669  smflimsuplem2  41670  smflimsuplem4  41672  smflimsuplem5  41673  smflimsuplem7  41675  smflimsup  41677
  Copyright terms: Public domain W3C validator