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

Metamath Proof Explorer

Theorem prodeq12i

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

Ref Expression
Hypotheses prodeq12i.1 ⊢ 𝐴 = 𝐵
prodeq12i.2 ⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 )
Assertion prodeq12i ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 prodeq12i.1 ⊢ 𝐴 = 𝐵
2 prodeq12i.2 ⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 )
3 2 prodeq2i ⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐴 𝐷
4 1 prodeq1i ⊢ ∏ 𝑘 ∈ 𝐴 𝐷 = ∏ 𝑘 ∈ 𝐵 𝐷
5 3 4 eqtri ⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐷