Metamath Proof Explorer


Theorem prodeq2dv

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

Ref Expression
Hypothesis prodeq2dv.1 ( ( 𝜑𝑘𝐴 ) → 𝐵 = 𝐶 )
Assertion prodeq2dv ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑘𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 prodeq2dv.1 ( ( 𝜑𝑘𝐴 ) → 𝐵 = 𝐶 )
2 1 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝐵 = 𝐶 )
3 2 prodeq2d ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑘𝐴 𝐶 )