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

Theorem supeq1d 8212
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 8211 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  supcsup 8206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-uni 4367  df-sup 8208
This theorem is referenced by:  supadd  10840  supminf  11609  rpnnen1lem6  11653  rpnnen1  11654  rpnnen1OLD  11659  limsupval  14001  limsupgval  14003  gcdval  15004  gcdass  15050  pcval  15335  pceulem  15336  pceu  15337  pczpre  15338  pcdiv  15343  pcneg  15364  prmreclem1  15406  prmreclem5  15410  ramz  15515  prdsval  15886  prdsdsval  15909  prdsdsval2  15915  prdsdsval3  15916  ressprdsds  21933  xpsdsval  21943  tmsxpsval  22100  bndth  22512  elovolmr  22995  ovolctb  23009  ovoliunlem3  23023  ovolshftlem1  23028  voliunlem3  23071  voliun  23073  volsup  23075  ioorf  23091  mbfinf  23182  itg1climres  23231  itg2val  23245  itg2monolem1  23267  itg2i1fseq  23272  itg2cnlem1  23278  mdegfval  23570  mdegval  23571  mdeg0  23578  mdegvsca  23584  mdegpropd  23592  deg1val  23604  deg1mul3  23623  dgrval  23732  coe11  23757  nmoofval  26794  nmooval  26795  nmoo0  26823  nmopval  27892  nmfnval  27912  esumval  29228  esum0  29231  esumsnf  29246  esumfsupre  29253  esumsup  29271  erdszelem3  30222  erdsze  30231  elwlim  30806  elwlimOLD  30807  ee7.2aOLD  31423  poimirlem32  32394  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  itg2addnc  32417  aomclem8  36432  supsubc  38293  fourierdlem79  38861  fourierdlem96  38878  fourierdlem97  38879  fourierdlem98  38880  fourierdlem99  38881  fourierdlem105  38887  fourierdlem108  38890  fourierdlem110  38892  sge0val  39042  sge0z  39051  sge0revalmpt  39054  sge0sn  39055  sge0tsms  39056  sge0f1o  39058  sge0sup  39067  sge0resplit  39082  meaiuninclem  39156
  Copyright terms: Public domain W3C validator