Theorem prodeq12si

Description: Equality inference for product. General version of prodeq2si . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	prodeq12si.1	⊢ 𝐴 = 𝐵
	prodeq12si.2	⊢ 𝐶 = 𝐷
Assertion	prodeq12si	⊢ ∏ 𝑥 ∈ 𝐴 𝐶 = ∏ 𝑥 ∈ 𝐵 𝐷

Proof

Step	Hyp	Ref	Expression
1		prodeq12si.1	⊢ 𝐴 = 𝐵
2		prodeq12si.2	⊢ 𝐶 = 𝐷
3	1	prodeq1i	⊢ ∏ 𝑥 ∈ 𝐴 𝐶 = ∏ 𝑥 ∈ 𝐵 𝐶
4	2	prodeq2si	⊢ ∏ 𝑥 ∈ 𝐵 𝐶 = ∏ 𝑥 ∈ 𝐵 𝐷
5	3 4	eqtri	⊢ ∏ 𝑥 ∈ 𝐴 𝐶 = ∏ 𝑥 ∈ 𝐵 𝐷