Theorem ixpeq12i

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

	Ref	Expression
Hypotheses	ixpeq12i.1	|- A = B
	ixpeq12i.2	|- C = D
Assertion	ixpeq12i	|- X_ x e. A C = X_ x e. B D

Proof

Step	Hyp	Ref	Expression
1		ixpeq12i.1	|- A = B
2		ixpeq12i.2	|- C = D
3	2	rgenw	|- A. x e. A C = D
4		ixpeq2	|- ( A. x e. A C = D -> X_ x e. A C = X_ x e. A D )
5	3 4	ax-mp	|- X_ x e. A C = X_ x e. A D
6	1	ixpeq1i	|- X_ x e. A D = X_ x e. B D
7	5 6	eqtri	|- X_ x e. A C = X_ x e. B D