Theorem cbvsumi 14653

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)

Hypotheses

Ref	Expression
cbvsumi.1	⊢ Ⅎ𝑘𝐵
cbvsumi.2	⊢ Ⅎ𝑗𝐶
cbvsumi.3	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)

Assertion

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

Distinct variable group:   𝑗,𝑘,𝐴

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

Proof of Theorem cbvsumi

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

Syntax hints:   → wi 4   = wceq 1637  Ⅎwnfc 2942  Σcsu 14642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-xp 5324  df-cnv 5326  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-iota 6067  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-seq 13028  df-sum 14643

This theorem is referenced by:  sumfc  14666  sumss2  14683  fsumzcl2  14695  fsumsplitf  14698  sumsnf  14699  sumsns  14705  fsummsnunz  14709  fsumsplitsnun  14710  fsummsnunzOLD  14711  fsumsplitsnunOLD  14712  fsum2dlem  14727  fsumcom2  14731  fsumshftm  14738  fsumrlim  14768  fsumo1  14769  o1fsum  14770  fsumiun  14778  ovolfiniun  23488  ovoliun2  23493  volfiniun  23534  itgfsum  23813  elplyd  24178  coeeq2  24218  fsumdvdscom  25131  fsumdvdsmul  25141  fsumvma  25158  fsumshftd  34733  binomcxplemdvsum  39055  sumsnd  39680  fourierdlem115  40918  fsummsndifre  41918  fsumsplitsndif  41919  fsummmodsndifre  41920  fsummmodsnunz  41921