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

Theorem esumeq1 30915
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 2796 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2esumeq12d 30914 1 (𝐴 = 𝐵 → Σ*𝑘𝐴𝐶 = Σ*𝑘𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1522  Σ*cesum 30908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-iota 6194  df-fv 6238  df-ov 7024  df-esum 30909
This theorem is referenced by:  esumrnmpt  30933  esumpad  30936  esumpad2  30937  esumpr  30947  esumpr2  30948  esumfzf  30950  esumpmono  30960  esumcvg  30967  esumcvg2  30968  esum2dlem  30973  measvun  31090  ddemeas  31117  oms0  31177  omssubadd  31180  carsgsigalem  31195  carsgclctunlem1  31197  carsgclctunlem2  31199  carsgclctun  31201  pmeasmono  31204  pmeasadd  31205
  Copyright terms: Public domain W3C validator