Theorem cbvprodi

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

	Ref	Expression
Hypotheses	cbvprodi.1	$$⊢\underset{\_}{Ⅎ}kB$$
	cbvprodi.2	$$⊢\underset{\_}{Ⅎ}jC$$
	cbvprodi.3	$$⊢j=k\to B=C$$
Assertion	cbvprodi	$$⊢\prod _{j\in A}B=\prod _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		cbvprodi.1	$$⊢\underset{\_}{Ⅎ}kB$$
2		cbvprodi.2	$$⊢\underset{\_}{Ⅎ}jC$$
3		cbvprodi.3	$$⊢j=k\to B=C$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
6	3 4 5 1 2	cbvprod	$$⊢\prod _{j\in A}B=\prod _{k\in A}C$$