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

Theorem supeq1d 8393
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 8392 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  supcsup 8387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-uni 4469  df-sup 8389
This theorem is referenced by:  supadd  11029  supminf  11813  rpnnen1lem6  11857  rpnnen1  11858  rpnnen1OLD  11863  limsupval  14249  limsupgval  14251  gcdval  15265  gcdass  15311  pcval  15596  pceulem  15597  pceu  15598  pczpre  15599  pcdiv  15604  pcneg  15625  prmreclem1  15667  prmreclem5  15671  ramz  15776  prdsval  16162  prdsdsval  16185  prdsdsval2  16191  prdsdsval3  16192  ressprdsds  22223  xpsdsval  22233  tmsxpsval  22390  bndth  22804  elovolmr  23290  ovolctb  23304  ovoliunlem3  23318  ovolshftlem1  23323  voliunlem3  23366  voliun  23368  volsup  23370  ioorf  23387  mbfinf  23477  itg1climres  23526  itg2val  23540  itg2monolem1  23562  itg2i1fseq  23567  itg2cnlem1  23573  mdegfval  23867  mdegval  23868  mdeg0  23875  mdegvsca  23881  mdegpropd  23889  deg1val  23901  deg1mul3  23920  dgrval  24029  coe11  24054  nmoofval  27745  nmooval  27746  nmoo0  27774  nmopval  28843  nmfnval  28863  esumval  30236  esum0  30239  esumsnf  30254  esumfsupre  30261  esumsup  30279  erdszelem3  31301  erdsze  31310  elwlim  31893  ee7.2aOLD  32585  poimirlem32  33571  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnc  33594  aomclem8  37948  infnsuprnmpt  39779  supsubc  39882  supxrmnf2  39973  supminfxr  40007  limsupval3  40242  limsupresre  40246  limsuplesup  40249  limsupresico  40250  limsupvaluz  40258  limsupvaluzmpt  40267  limsupvaluz2  40288  supcnvlimsup  40290  supcnvlimsupmpt  40291  limsuplt2  40303  liminfval  40309  limsupge  40311  liminfval5  40315  limsupresxr  40316  liminfresxr  40317  liminfresico  40321  limsup10ex  40323  liminflelimsuplem  40325  fourierdlem79  40720  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem105  40746  fourierdlem108  40749  fourierdlem110  40751  sge0val  40901  sge0z  40910  sge0revalmpt  40913  sge0sn  40914  sge0tsms  40915  sge0f1o  40917  sge0sup  40926  sge0resplit  40941  meaiuninclem  41015  smfsuplem2  41339  smfsup  41341  smfsupmpt  41342  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem4  41350  smflimsuplem5  41351  smflimsuplem7  41353  smflimsup  41355
  Copyright terms: Public domain W3C validator