Theorem cbvsumv 11747

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 2349	. 2 ⊢ Ⅎ𝑘𝐴
3		nfcv 2349	. 2 ⊢ Ⅎ𝑗𝐴
4		nfcv 2349	. 2 ⊢ Ⅎ𝑘𝐵
5		nfcv 2349	. 2 ⊢ Ⅎ𝑗𝐶
6	1, 2, 3, 4, 5	cbvsum 11746	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1373  Σcsu 11739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-un 3174  df-in 3176  df-ss 3183  df-if 3576  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-mpt 4115  df-cnv 4691  df-dm 4693  df-rn 4694  df-res 4695  df-iota 5241  df-fv 5288  df-ov 5960  df-oprab 5961  df-mpo 5962  df-recs 6404  df-frec 6490  df-seqfrec 10615  df-sumdc 11740

This theorem is referenced by:  isumge0  11816  telfsumo  11852  fsumparts  11856  binomlem  11869  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  efaddlem  12060  plymullem1  15295  plyadd  15298  plymul  15299  plycoeid3  15304  plyco  15306  plycj  15308  dvply1  15312  trilpo  16123  redcwlpo  16135  nconstwlpo  16146  neapmkv  16148