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 -> C = D )
	cbvixpvw2.2	|- ( x = y -> A = B )
Assertion	cbvixpvw2	|- X_ x e. A C = X_ y e. B D

Proof

Step	Hyp	Ref	Expression
1		cbvixpvw2.1	|- ( x = y -> C = D )
2		cbvixpvw2.2	|- ( x = y -> A = B )
3		id	|- ( x = y -> x = y )
4	3 2	eleq12d	|- ( x = y -> ( x e. A <-> y e. B ) )
5	4	cbvabv	|- { x | x e. A } = { y | y e. B }
6	5	fneq2i	|- ( t Fn { x | x e. A } <-> t Fn { y | y e. B } )
7		fveq2	|- ( x = y -> ( t ` x ) = ( t ` y ) )
8	7 1	eleq12d	|- ( x = y -> ( ( t ` x ) e. C <-> ( t ` y ) e. D ) )
9	2 8	cbvralvw2	|- ( A. x e. A ( t ` x ) e. C <-> A. y e. B ( t ` y ) e. D )
10	6 9	anbi12i	|- ( ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) <-> ( t Fn { y | y e. B } /\ A. y e. B ( t ` y ) e. D ) )
11	10	abbii	|- { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) } = { t | ( t Fn { y | y e. B } /\ A. y e. B ( t ` y ) e. D ) }
12		df-ixp	|- X_ x e. A C = { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) }
13		df-ixp	|- X_ y e. B D = { t | ( t Fn { y | y e. B } /\ A. y e. B ( t ` y ) e. D ) }
14	11 12 13	3eqtr4i	|- X_ x e. A C = X_ y e. B D