This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prodeq12i

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

Step	Hyp	Ref	Expression
1		prodeq12i.1	$⊢ A = B$
2		prodeq12i.2	$⊢ k \in A \to C = D$
3	2	prodeq2i	$⊢ \prod_{k \in A} C = \prod_{k \in A} D$
4	1	prodeq1i	$⊢ \prod_{k \in A} D = \prod_{k \in B} D$
5	3 4	eqtri	$⊢ \prod_{k \in A} C = \prod_{k \in B} D$