# Metamath Proof Explorer

## Theorem cbvprod

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses cbvprod.1 ${⊢}{j}={k}\to {B}={C}$
cbvprod.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
cbvprod.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
cbvprod.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
cbvprod.5 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
Assertion cbvprod ${⊢}\prod _{{j}\in {A}}{B}=\prod _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 cbvprod.1 ${⊢}{j}={k}\to {B}={C}$
2 cbvprod.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvprod.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
4 cbvprod.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
5 cbvprod.5 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
6 biid ${⊢}{A}\subseteq {ℤ}_{\ge {m}}↔{A}\subseteq {ℤ}_{\ge {m}}$
7 2 nfcri ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{j}\in {A}$
8 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}1$
9 7 4 8 nfif ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}if\left({j}\in {A},{B},1\right)$
10 3 nfcri ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{k}\in {A}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}1$
12 10 5 11 nfif ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{C},1\right)$
13 eleq1w ${⊢}{j}={k}\to \left({j}\in {A}↔{k}\in {A}\right)$
14 13 1 ifbieq1d ${⊢}{j}={k}\to if\left({j}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)$
15 9 12 14 cbvmpt ${⊢}\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)$
16 seqeq3 ${⊢}\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\to seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)=seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
17 15 16 ax-mp ${⊢}seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)=seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
18 17 breq1i ${⊢}seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}↔seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}$
19 18 anbi2i ${⊢}\left({y}\ne 0\wedge seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}\right)↔\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)$
20 19 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)$
21 20 rexbii ${⊢}\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}\right)↔\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)$
22 seqeq3 ${⊢}\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\to seq{m}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)=seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
23 15 22 ax-mp ${⊢}seq{m}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)=seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
24 23 breq1i ${⊢}seq{m}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{x}↔seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}$
25 6 21 24 3anbi123i ${⊢}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{x}\right)↔\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}\right)$
26 25 rexbii ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({j}\in ℤ⟼if\left({j}\in {A},{B},1\right)\right)\right)⇝{x}\right)↔\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}\right)$
27 4 5 1 cbvcsbw
28 27 mpteq2i
29 seqeq3
30 28 29 ax-mp
31 30 fveq1i
32 31 eqeq2i
33 32 anbi2i
34 33 exbii
35 34 rexbii
36 26 35 orbi12i
37 36 iotabii
38 df-prod
39 df-prod
40 37 38 39 3eqtr4i ${⊢}\prod _{{j}\in {A}}{B}=\prod _{{k}\in {A}}{C}$