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

Theorem esumeq1 28263
Description: Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)
Assertion
Ref Expression
esumeq1  |-  ( A  =  B  -> Σ* k  e.  A C  = Σ* k  e.  B C )
Distinct variable groups:    A, k    B, k
Allowed substitution hint:    C( k)

Proof of Theorem esumeq1
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
2 eqidd 2455 . 2  |-  ( A  =  B  ->  C  =  C )
31, 2esumeq12d 28262 1  |-  ( A  =  B  -> Σ* k  e.  A C  = Σ* k  e.  B C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398  Σ*cesum 28256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-iota 5534  df-fv 5578  df-ov 6273  df-esum 28257
This theorem is referenced by:  esumrnmpt  28281  esumpad  28284  esumpad2  28285  esumpr  28295  esumpr2  28296  esumfzf  28298  esumpmono  28308  esumcvg  28315  esumcvg2  28316  esum2dlem  28321  measvun  28417  ddemeas  28445  oms0  28505  omssubadd  28508  carsgsigalem  28523  carsgclctunlem1  28525  carsgclctunlem2  28527  carsgclctun  28529
  Copyright terms: Public domain W3C validator