Theorem cbvprodi

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

	Ref	Expression
Hypotheses	cbvprodi.1	|- F/_ k B
	cbvprodi.2	|- F/_ j C
	cbvprodi.3	|- ( j = k -> B = C )
Assertion	cbvprodi	|- prod_ j e. A B = prod_ k e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvprodi.1	|- F/_ k B
2		cbvprodi.2	|- F/_ j C
3		cbvprodi.3	|- ( j = k -> B = C )
4		nfcv	|- F/_ k A
5		nfcv	|- F/_ j A
6	3 4 5 1 2	cbvprod	|- prod_ j e. A B = prod_ k e. A C