Theorem ixpeq12i

Description: Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	ixpeq12i.1	⊢ 𝐴 = 𝐵
	ixpeq12i.2	⊢ 𝐶 = 𝐷
Assertion	ixpeq12i	⊢ X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐷

Proof

Step	Hyp	Ref	Expression
1		ixpeq12i.1	⊢ 𝐴 = 𝐵
2		ixpeq12i.2	⊢ 𝐶 = 𝐷
3	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷
4		ixpeq2	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 → X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐴 𝐷 )
5	3 4	ax-mp	⊢ X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐴 𝐷
6	1	ixpeq1i	⊢ X 𝑥 ∈ 𝐴 𝐷 = X 𝑥 ∈ 𝐵 𝐷
7	5 6	eqtri	⊢ X 𝑥 ∈ 𝐴 𝐶 = X 𝑥 ∈ 𝐵 𝐷