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

Theorem cbvsumv 13498
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 2629 . 2  |-  F/_ k A
3 nfcv 2629 . 2  |-  F/_ j A
4 nfcv 2629 . 2  |-  F/_ k B
5 nfcv 2629 . 2  |-  F/_ j C
61, 2, 3, 4, 5cbvsum 13497 1  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   sum_csu 13488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-cnv 5013  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-recs 7054  df-rdg 7088  df-seq 12088  df-sum 13489
This theorem is referenced by:  isumge0  13561  telfsumo  13596  fsumparts  13600  binomlem  13621  incexclem  13628  mertenslem1  13673  mertens  13675  efaddlem  13707  bitsinv2  13969  prmreclem6  14315  ovolicc2lem4  21799  uniioombllem6  21865  plymullem1  22479  plyadd  22482  plymul  22483  coeeu  22490  coeid  22503  dvply1  22547  vieta1  22575  aaliou3  22614  abelthlem8  22701  abelthlem9  22702  abelth  22703  logtayl  22907  ftalem2  23213  ftalem6  23217  dchrsum2  23409  sumdchr2  23411  dchrisumlem1  23540  dchrisum  23543  dchrisum0fval  23556  dchrisum0ff  23558  rpvmasum  23577  mulog2sumlem1  23585  2vmadivsumlem  23591  logsqvma  23593  logsqvma2  23594  selberg  23599  chpdifbndlem1  23604  selberg3lem1  23608  selberg4lem1  23611  pntsval  23623  pntsval2  23627  pntpbnd1  23637  pntlemo  23658  axsegconlem9  24051  hashunif  27428  eulerpartlems  28124  eulerpartlemgs2  28144  binomfallfaclem2  29089  bpolyval  29738  sumnnodd  31495  fourierdlem112  31842  fourierdlem113  31843  altgsumbcALT  32421
  Copyright terms: Public domain W3C validator