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	$$⊢\underset{x\in A}{⨉}C=\underset{x\in B}{⨉}D$$

Proof

Step	Hyp	Ref	Expression
1		ixpeq12i.1	$$⊢A=B$$
2		ixpeq12i.2	$$⊢C=D$$
3	2	rgenw	$$⊢\forall x\in AC=D$$
4		ixpeq2	$$⊢\forall x\in AC=D\to \underset{x\in A}{⨉}C=\underset{x\in A}{⨉}D$$
5	3 4	ax-mp	$$⊢\underset{x\in A}{⨉}C=\underset{x\in A}{⨉}D$$
6	1	ixpeq1i	$$⊢\underset{x\in A}{⨉}D=\underset{x\in B}{⨉}D$$
7	5 6	eqtri	$$⊢\underset{x\in A}{⨉}C=\underset{x\in B}{⨉}D$$