![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvsumi | Structured version Visualization version GIF version |
Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
Ref | Expression |
---|---|
cbvsumi.1 | ⊢ Ⅎ𝑘𝐵 |
cbvsumi.2 | ⊢ Ⅎ𝑗𝐶 |
cbvsumi.3 | ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvsumi | ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvsumi.3 | . 2 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) | |
2 | nfcv 2891 | . 2 ⊢ Ⅎ𝑘𝐴 | |
3 | nfcv 2891 | . 2 ⊢ Ⅎ𝑗𝐴 | |
4 | cbvsumi.1 | . 2 ⊢ Ⅎ𝑘𝐵 | |
5 | cbvsumi.2 | . 2 ⊢ Ⅎ𝑗𝐶 | |
6 | 1, 2, 3, 4, 5 | cbvsum 15677 | 1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 Ⅎwnfc 2875 Σcsu 15668 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-xp 5684 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-iota 6501 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-seq 14003 df-sum 15669 |
This theorem is referenced by: sumfc 15691 sumss2 15708 fsumzcl2 15721 fsumsplitf 15724 sumsnf 15725 sumsns 15732 fsummsnunz 15736 fsumsplitsnun 15737 fsum2dlem 15752 fsumcom2 15756 fsumshftm 15763 fsumrlim 15793 fsumo1 15794 o1fsum 15795 fsumiun 15803 ovolfiniun 25474 ovoliun2 25479 volfiniun 25520 itgfsum 25800 elplyd 26181 coeeq2 26221 fsumdvdscom 27162 fsumdvdsmul 27172 fsumdvdsmulOLD 27174 fsumvma 27191 fsumshftd 38554 binomcxplemdvsum 43934 sumsnd 44530 fourierdlem115 45747 fsummsndifre 46849 fsumsplitsndif 46850 fsummmodsndifre 46851 fsummmodsnunz 46852 |
Copyright terms: Public domain | W3C validator |