Description: Equality deduction for product. (Contributed by Scott Fenton, 4Dec2017)
Ref  Expression  

Hypothesis  prodeq2dv.1   ( ( ph /\ k e. A ) > B = C ) 

Assertion  prodeq2dv   ( ph > prod_ k e. A B = prod_ k e. A C ) 
Step  Hyp  Ref  Expression 

1  prodeq2dv.1   ( ( ph /\ k e. A ) > B = C ) 

2  1  ralrimiva   ( ph > A. k e. A B = C ) 
3  2  prodeq2d   ( ph > prod_ k e. A B = prod_ k e. A C ) 