Theorem cbvixpvw2

Description: Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvixpvw2.1	$$⊢x=y\to C=D$$
	cbvixpvw2.2	$$⊢x=y\to A=B$$
Assertion	cbvixpvw2	$$⊢\underset{x\in A}{⨉}C=\underset{y\in B}{⨉}D$$

Proof

Step	Hyp	Ref	Expression
1		cbvixpvw2.1	$$⊢x=y\to C=D$$
2		cbvixpvw2.2	$$⊢x=y\to A=B$$
3		id	$$⊢x=y\to x=y$$
4	3 2	eleq12d	$$⊢x=y\to \left(x\in A\leftrightarrow y\in B\right)$$
5	4	cbvabv	$$⊢\left\{x|x\in A\right\}=\left\{y|y\in B\right\}$$
6	5	fneq2i	$$⊢tFn\left\{x|x\in A\right\}\leftrightarrow tFn\left\{y|y\in B\right\}$$
7		fveq2	$$⊢x=y\to t\left(x\right)=t\left(y\right)$$
8	7 1	eleq12d	$$⊢x=y\to \left(t\left(x\right)\in C\leftrightarrow t\left(y\right)\in D\right)$$
9	2 8	cbvralvw2	$$⊢\forall x\in At\left(x\right)\in C\leftrightarrow \forall y\in Bt\left(y\right)\in D$$
10	6 9	anbi12i	$$⊢\left(tFn\left\{x|x\in A\right\}\wedge \forall x\in At\left(x\right)\in C\right)\leftrightarrow \left(tFn\left\{y|y\in B\right\}\wedge \forall y\in Bt\left(y\right)\in D\right)$$
11	10	abbii	$$⊢\left\{t|\left(tFn\left\{x|x\in A\right\}\wedge \forall x\in At\left(x\right)\in C\right)\right\}=\left\{t|\left(tFn\left\{y|y\in B\right\}\wedge \forall y\in Bt\left(y\right)\in D\right)\right\}$$
12		df-ixp	$$⊢\underset{x\in A}{⨉}C=\left\{t|\left(tFn\left\{x|x\in A\right\}\wedge \forall x\in At\left(x\right)\in C\right)\right\}$$
13		df-ixp	$$⊢\underset{y\in B}{⨉}D=\left\{t|\left(tFn\left\{y|y\in B\right\}\wedge \forall y\in Bt\left(y\right)\in D\right)\right\}$$
14	11 12 13	3eqtr4i	$$⊢\underset{x\in A}{⨉}C=\underset{y\in B}{⨉}D$$