Metamath Proof Explorer
Description: Equality deduction for product. Note that unlike prodeq2dv , k
may occur in ph . (Contributed by Scott Fenton, 4Dec2017)


Ref 
Expression 

Hypothesis 
prodeq2d.1 
$${\u22a2}{\phi}\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}$$ 

Assertion 
prodeq2d 
$${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

prodeq2d.1 
$${\u22a2}{\phi}\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}$$ 
2 

prodeq2 
$${\u22a2}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ 
3 
1 2

syl 
$${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ 