Theorem cbvprodv

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

	Ref	Expression
Hypothesis	cbvprod.1	$$⊢j=k\to B=C$$
Assertion	cbvprodv	$$⊢\prod _{j\in A}B=\prod _{k\in A}C$$

Proof

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