Theorem cbvsumv 15649

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	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvsumv	⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Distinct variable groups:   𝑗,𝑘,𝐴   𝐵,𝑘   𝐶,𝑗

Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑘)

Proof of Theorem cbvsumv

Step	Hyp	Ref	Expression
1		cbvsum.1	. 2 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
2		nfcv 2902	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2902	. 2 ⊢ Ⅎ𝑗𝐴
4		nfcv 2902	. 2 ⊢ Ⅎ𝑘𝐵
5		nfcv 2902	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 15648	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540  Σcsu 15639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-11 2153  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-seq 13974  df-sum 15640

This theorem is referenced by:  isumge0  15719  telfsumo  15755  fsumparts  15759  binomlem  15782  incexclem  15789  pwdif  15821  mertenslem1  15837  mertens  15839  binomfallfaclem2  15991  bpolyval  16000  efaddlem  16043  pwp1fsum  16341  bitsinv2  16391  prmreclem6  16861  ovolicc2lem4  25282  uniioombllem6  25350  plymullem1  25977  plyadd  25980  plymul  25981  coeeu  25988  coeid  26001  dvply1  26047  vieta1  26075  aaliou3  26114  abelthlem8  26202  abelthlem9  26203  abelth  26204  logtayl  26419  ftalem2  26829  ftalem6  26833  dchrsum2  27022  sumdchr2  27024  dchrisumlem1  27243  dchrisum  27246  dchrisum0fval  27259  dchrisum0ff  27261  rpvmasum  27280  mulog2sumlem1  27288  2vmadivsumlem  27294  logsqvma  27296  logsqvma2  27297  selberg  27302  chpdifbndlem1  27307  selberg3lem1  27311  selberg4lem1  27314  pntsval  27326  pntsval2  27330  pntpbnd1  27340  pntlemo  27361  axsegconlem9  28465  hashunif  32300  eulerpartlems  33672  eulerpartlemgs2  33692  breprexplema  33955  breprexplemc  33957  breprexp  33958  hgt750lema  33982  fwddifnp1  35456  sticksstones16  41297  sticksstones17  41298  sticksstones18  41299  sticksstones21  41302  binomcxplemnotnn0  43430  mccl  44625  sumnnodd  44657  dvnprodlem1  44973  dvnprodlem3  44975  dvnprod  44976  fourierdlem73  45206  fourierdlem112  45245  fourierdlem113  45246  etransclem11  45272  etransclem32  45293  etransclem35  45296  etransc  45310  fsumlesge0  45404  meaiuninclem  45507  omeiunltfirp  45546  hoidmvlelem3  45624  altgsumbcALT  47130  nn0sumshdiglemA  47405  nn0sumshdiglemB  47406