Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumeq1 Structured version   Visualization version   GIF version

Theorem esumeq1 31469
 Description: Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
Assertion
Ref Expression
esumeq1 (𝐴 = 𝐵 → Σ*𝑘𝐴𝐶 = Σ*𝑘𝐵𝐶)
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘
Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem esumeq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
2 eqidd 2799 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2esumeq12d 31468 1 (𝐴 = 𝐵 → Σ*𝑘𝐴𝐶 = Σ*𝑘𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  Σ*cesum 31462 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3444  df-un 3888  df-in 3890  df-ss 3900  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-iota 6291  df-fv 6340  df-ov 7148  df-esum 31463 This theorem is referenced by:  esumrnmpt  31487  esumpad  31490  esumpad2  31491  esumpr  31501  esumpr2  31502  esumfzf  31504  esumpmono  31514  esumcvg  31521  esumcvg2  31522  esum2dlem  31527  measvun  31644  ddemeas  31671  oms0  31731  omssubadd  31734  carsgsigalem  31749  carsgclctunlem1  31751  carsgclctunlem2  31753  carsgclctun  31755  pmeasmono  31758  pmeasadd  31759
 Copyright terms: Public domain W3C validator