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

Theorem cbvsumv 12266
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 2494 . 2  |-  F/_ k A
3 nfcv 2494 . 2  |-  F/_ j A
4 nfcv 2494 . 2  |-  F/_ k B
5 nfcv 2494 . 2  |-  F/_ j C
61, 2, 3, 4, 5cbvsum 12265 1  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   sum_csu 12255
This theorem is referenced by:  isumge0  12326  fsumtscopo  12357  fsumparts  12361  binomlem  12384  incexclem  12392  mertenslem1  12437  mertens  12439  efaddlem  12471  bitsinv2  12731  prmreclem6  13065  ovolicc2lem4  18983  uniioombllem6  19047  plymullem1  19700  plyadd  19703  plymul  19704  coeeu  19711  coeid  19724  dvply1  19768  vieta1  19796  aaliou3  19835  abelthlem8  19922  abelthlem9  19923  abelth  19924  logtayl  20118  ftalem2  20423  ftalem6  20427  dchrsum2  20619  sumdchr2  20621  dchrisumlem1  20750  dchrisum  20753  dchrisum0fval  20766  dchrisum0ff  20768  rpvmasum  20787  mulog2sumlem1  20795  2vmadivsumlem  20801  logsqvma  20803  logsqvma2  20804  selberg  20809  chpdifbndlem1  20814  selberg3lem1  20818  selberg4lem1  20821  pntsval  20833  pntsval2  20837  pntpbnd1  20847  pntlemo  20868  axsegconlem9  25112  bpolyval  25343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-cnv 4779  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-recs 6475  df-rdg 6510  df-seq 11139  df-sum 12256
  Copyright terms: Public domain W3C validator