![]() |
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 2934 | . 2 ⊢ Ⅎ𝑘𝐴 | |
3 | nfcv 2934 | . 2 ⊢ Ⅎ𝑗𝐴 | |
4 | cbvsumi.1 | . 2 ⊢ Ⅎ𝑘𝐵 | |
5 | cbvsumi.2 | . 2 ⊢ Ⅎ𝑗𝐶 | |
6 | 1, 2, 3, 4, 5 | cbvsum 14842 | 1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 Ⅎwnfc 2919 Σcsu 14833 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-mpt 4968 df-xp 5363 df-cnv 5365 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-pred 5935 df-iota 6101 df-fv 6145 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-wrecs 7691 df-recs 7753 df-rdg 7791 df-seq 13125 df-sum 14834 |
This theorem is referenced by: sumfc 14856 sumss2 14873 fsumzcl2 14885 fsumsplitf 14888 sumsnf 14889 sumsns 14895 fsummsnunz 14899 fsumsplitsnun 14900 fsum2dlem 14915 fsumcom2 14919 fsumshftm 14926 fsumrlim 14956 fsumo1 14957 o1fsum 14958 fsumiun 14966 ovolfiniun 23716 ovoliun2 23721 volfiniun 23762 itgfsum 24041 elplyd 24406 coeeq2 24446 fsumdvdscom 25374 fsumdvdsmul 25384 fsumvma 25401 fsumshftd 35115 binomcxplemdvsum 39524 sumsnd 40132 fourierdlem115 41379 fsummsndifre 42388 fsumsplitsndif 42389 fsummmodsndifre 42390 fsummmodsnunz 42391 |
Copyright terms: Public domain | W3C validator |