Theorem prodeq1i

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

	Ref	Expression
Hypothesis	prodeq1i.1	|- A = B
Assertion	prodeq1i	|- prod_ k e. A C = prod_ k e. B C

Proof

Step	Hyp	Ref	Expression
1		prodeq1i.1	|- A = B
2		prodeq1	|- ( A = B -> prod_ k e. A C = prod_ k e. B C )
3	1 2	ax-mp	|- prod_ k e. A C = prod_ k e. B C