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

Theorem supeq1d 8520
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 8519 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  supcsup 8514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-uni 4590  df-sup 8516
This theorem is referenced by:  supadd  11204  supminf  11989  rpnnen1lem6  12033  rpnnen1  12034  rpnnen1OLD  12039  limsupval  14425  limsupgval  14427  gcdval  15441  gcdass  15487  pcval  15772  pceulem  15773  pceu  15774  pczpre  15775  pcdiv  15780  pcneg  15801  prmreclem1  15843  prmreclem5  15847  ramz  15952  prdsval  16338  prdsdsval  16361  prdsdsval2  16367  prdsdsval3  16368  ressprdsds  22398  xpsdsval  22408  tmsxpsval  22565  bndth  22979  elovolmr  23465  ovolctb  23479  ovoliunlem3  23493  ovolshftlem1  23498  voliunlem3  23541  voliun  23543  volsup  23545  ioorf  23562  mbfinf  23652  itg1climres  23701  itg2val  23715  itg2monolem1  23737  itg2i1fseq  23742  itg2cnlem1  23748  mdegfval  24042  mdegval  24043  mdeg0  24050  mdegvsca  24056  mdegpropd  24064  deg1val  24076  deg1mul3  24095  dgrval  24204  coe11  24229  nmoofval  27948  nmooval  27949  nmoo0  27977  nmopval  29046  nmfnval  29066  esumval  30439  esum0  30442  esumsnf  30457  esumfsupre  30464  esumsup  30482  erdszelem3  31504  erdsze  31513  elwlim  32096  ee7.2aOLD  32788  poimirlem32  33773  ovoliunnfl  33783  voliunnfl  33785  volsupnfl  33786  itg2addnc  33796  aomclem8  38152  infnsuprnmpt  39983  supsubc  40086  supxrmnf2  40177  supminfxr  40211  limsupval3  40446  limsupresre  40450  limsuplesup  40453  limsupresico  40454  limsupvaluz  40462  limsupvaluzmpt  40471  limsupvaluz2  40492  supcnvlimsup  40494  supcnvlimsupmpt  40495  limsuplt2  40507  liminfval  40513  limsupge  40515  liminfval5  40519  limsupresxr  40520  liminfresxr  40521  liminfresico  40525  limsup10ex  40527  liminflelimsuplem  40529  fourierdlem79  40924  fourierdlem96  40941  fourierdlem97  40942  fourierdlem98  40943  fourierdlem99  40944  fourierdlem105  40950  fourierdlem108  40953  fourierdlem110  40955  sge0val  41105  sge0z  41114  sge0revalmpt  41117  sge0sn  41118  sge0tsms  41119  sge0f1o  41121  sge0sup  41130  sge0resplit  41145  meaiuninclem  41219  smfsuplem2  41543  smfsup  41545  smfsupmpt  41546  smflimsuplem1  41551  smflimsuplem2  41552  smflimsuplem4  41554  smflimsuplem5  41555  smflimsuplem7  41557  smflimsup  41559
  Copyright terms: Public domain W3C validator