Metamath Proof Explorer


Theorem prodeq12i

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

Ref Expression
Hypotheses prodeq12i.1
|- A = B
prodeq12i.2
|- ( k e. A -> C = D )
Assertion prodeq12i
|- prod_ k e. A C = prod_ k e. B D

Proof

Step Hyp Ref Expression
1 prodeq12i.1
 |-  A = B
2 prodeq12i.2
 |-  ( k e. A -> C = D )
3 2 prodeq2i
 |-  prod_ k e. A C = prod_ k e. A D
4 1 prodeq1i
 |-  prod_ k e. A D = prod_ k e. B D
5 3 4 eqtri
 |-  prod_ k e. A C = prod_ k e. B D