Theorem cbvixpv

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypothesis	cbvixpv.1	$$⊢x=y\to B=C$$
Assertion	cbvixpv	$$⊢\underset{x\in A}{⨉}B=\underset{y\in A}{⨉}C$$

Proof

Step	Hyp	Ref	Expression
1		cbvixpv.1	$$⊢x=y\to B=C$$
2		fveq2	$$⊢x=y\to z\left(x\right)=z\left(y\right)$$
3	2 1	eleq12d	$$⊢x=y\to \left(z\left(x\right)\in B\leftrightarrow z\left(y\right)\in C\right)$$
4	3	cbvralvw	$$⊢\forall x\in Az\left(x\right)\in B\leftrightarrow \forall y\in Az\left(y\right)\in C$$
5	4	anbi2i	$$⊢\left(zFnA\wedge \forall x\in Az\left(x\right)\in B\right)\leftrightarrow \left(zFnA\wedge \forall y\in Az\left(y\right)\in C\right)$$
6	5	abbii	$$⊢\left\{z|\left(zFnA\wedge \forall x\in Az\left(x\right)\in B\right)\right\}=\left\{z|\left(zFnA\wedge \forall y\in Az\left(y\right)\in C\right)\right\}$$
7		dfixp	$$⊢\underset{x\in A}{⨉}B=\left\{z|\left(zFnA\wedge \forall x\in Az\left(x\right)\in B\right)\right\}$$
8		dfixp	$$⊢\underset{y\in A}{⨉}C=\left\{z|\left(zFnA\wedge \forall y\in Az\left(y\right)\in C\right)\right\}$$
9	6 7 8	3eqtr4i	$$⊢\underset{x\in A}{⨉}B=\underset{y\in A}{⨉}C$$