MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvsumv Structured version   Unicode version

Theorem cbvsumv 13173
Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
Hypothesis
Ref Expression
cbvsum.1  |-  ( j  =  k  ->  B  =  C )
Assertion
Ref Expression
cbvsumv  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Distinct variable groups:    j, k, A    B, k    C, j
Allowed substitution hints:    B( j)    C( k)

Proof of Theorem cbvsumv
StepHypRef Expression
1 cbvsum.1 . 2  |-  ( j  =  k  ->  B  =  C )
2 nfcv 2579 . 2  |-  F/_ k A
3 nfcv 2579 . 2  |-  F/_ j A
4 nfcv 2579 . 2  |-  F/_ k B
5 nfcv 2579 . 2  |-  F/_ j C
61, 2, 3, 4, 5cbvsum 13172 1  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   sum_csu 13163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-cnv 4848  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-recs 6832  df-rdg 6866  df-seq 11807  df-sum 13164
This theorem is referenced by:  isumge0  13233  fsumtscopo  13265  fsumparts  13269  binomlem  13292  incexclem  13299  mertenslem1  13344  mertens  13346  efaddlem  13378  bitsinv2  13639  prmreclem6  13982  ovolicc2lem4  21003  uniioombllem6  21068  plymullem1  21682  plyadd  21685  plymul  21686  coeeu  21693  coeid  21706  dvply1  21750  vieta1  21778  aaliou3  21817  abelthlem8  21904  abelthlem9  21905  abelth  21906  logtayl  22105  ftalem2  22411  ftalem6  22415  dchrsum2  22607  sumdchr2  22609  dchrisumlem1  22738  dchrisum  22741  dchrisum0fval  22754  dchrisum0ff  22756  rpvmasum  22775  mulog2sumlem1  22783  2vmadivsumlem  22789  logsqvma  22791  logsqvma2  22792  selberg  22797  chpdifbndlem1  22802  selberg3lem1  22806  selberg4lem1  22809  pntsval  22821  pntsval2  22825  pntpbnd1  22835  pntlemo  22856  axsegconlem9  23171  hashunif  26084  eulerpartlems  26743  eulerpartlemgs2  26763  binomfallfaclem2  27543  bpolyval  28192  altgsumbcALT  30750
  Copyright terms: Public domain W3C validator