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

Theorem cbvsumv 13169
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 2577 . 2  |-  F/_ k A
3 nfcv 2577 . 2  |-  F/_ j A
4 nfcv 2577 . 2  |-  F/_ k B
5 nfcv 2577 . 2  |-  F/_ j C
61, 2, 3, 4, 5cbvsum 13168 1  |-  sum_ j  e.  A  B  =  sum_ k  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   sum_csu 13159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-recs 6828  df-rdg 6862  df-seq 11803  df-sum 13160
This theorem is referenced by:  isumge0  13229  fsumtscopo  13261  fsumparts  13265  binomlem  13288  incexclem  13295  mertenslem1  13340  mertens  13342  efaddlem  13374  bitsinv2  13635  prmreclem6  13978  ovolicc2lem4  20903  uniioombllem6  20968  plymullem1  21625  plyadd  21628  plymul  21629  coeeu  21636  coeid  21649  dvply1  21693  vieta1  21721  aaliou3  21760  abelthlem8  21847  abelthlem9  21848  abelth  21849  logtayl  22048  ftalem2  22354  ftalem6  22358  dchrsum2  22550  sumdchr2  22552  dchrisumlem1  22681  dchrisum  22684  dchrisum0fval  22697  dchrisum0ff  22699  rpvmasum  22718  mulog2sumlem1  22726  2vmadivsumlem  22732  logsqvma  22734  logsqvma2  22735  selberg  22740  chpdifbndlem1  22745  selberg3lem1  22749  selberg4lem1  22752  pntsval  22764  pntsval2  22768  pntpbnd1  22778  pntlemo  22799  axsegconlem9  23090  hashunif  26001  eulerpartlems  26657  eulerpartlemgs2  26677  binomfallfaclem2  27456  bpolyval  28105  altgsumbc  30650
  Copyright terms: Public domain W3C validator