Theorem prodeq2

Description: Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Assertion	prodeq2	$$⊢\forall k\in AB=C\to \prod _{k\in A}B=\prod _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢B=C\to \mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)$$
2	1	ralimi	$$⊢\forall k\in AB=C\to \forall k\in A\mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)$$
3		prodeq2ii	$$⊢\forall k\in A\mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)\to \prod _{k\in A}B=\prod _{k\in A}C$$
4	2 3	syl	$$⊢\forall k\in AB=C\to \prod _{k\in A}B=\prod _{k\in A}C$$