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

Metamath Proof Explorer

Theorem prodeq12dv

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

Ref Expression
Hypotheses prodeq12dv.1 ⊢ φ → A = B
prodeq12dv.2 ⊢ φ ∧ k ∈ A → C = D
Assertion prodeq12dv ⊢ φ → ∏ k ∈ A C = ∏ k ∈ B D

Proof

Step Hyp Ref Expression
1 prodeq12dv.1 ⊢ φ → A = B
2 prodeq12dv.2 ⊢ φ ∧ k ∈ A → C = D
3 2 prodeq2dv ⊢ φ → ∏ k ∈ A C = ∏ k ∈ A D
4 1 prodeq1d ⊢ φ → ∏ k ∈ A D = ∏ k ∈ B D
5 3 4 eqtrd ⊢ φ → ∏ k ∈ A C = ∏ k ∈ B D