Theorem cbvixpdavw2

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

	Ref	Expression
Hypotheses	cbvixpdavw2.1	|- ( ( ph /\ x = y ) -> C = D )
	cbvixpdavw2.2	|- ( ( ph /\ x = y ) -> A = B )
Assertion	cbvixpdavw2	|- ( ph -> X_ x e. A C = X_ y e. B D )

Proof

Step	Hyp	Ref	Expression
1		cbvixpdavw2.1	|- ( ( ph /\ x = y ) -> C = D )
2		cbvixpdavw2.2	|- ( ( ph /\ x = y ) -> A = B )
3		simpr	|- ( ( ph /\ x = y ) -> x = y )
4	3 2	eleq12d	|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. B ) )
5	4	cbvabdavw	|- ( ph -> { x | x e. A } = { y | y e. B } )
6	5	fneq2d	|- ( ph -> ( t Fn { x | x e. A } <-> t Fn { y | y e. B } ) )
7		fveq2	|- ( x = y -> ( t ` x ) = ( t ` y ) )
8	7	adantl	|- ( ( ph /\ x = y ) -> ( t ` x ) = ( t ` y ) )
9	8 1	eleq12d	|- ( ( ph /\ x = y ) -> ( ( t ` x ) e. C <-> ( t ` y ) e. D ) )
10	9 2	cbvraldva2	|- ( ph -> ( A. x e. A ( t ` x ) e. C <-> A. y e. B ( t ` y ) e. D ) )
11	6 10	anbi12d	|- ( ph -> ( ( 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 ) ) )
12	11	abbidv	|- ( ph -> { 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 ) } )
13		df-ixp	|- X_ x e. A C = { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) }
14		df-ixp	|- X_ y e. B D = { t | ( t Fn { y | y e. B } /\ A. y e. B ( t ` y ) e. D ) }
15	12 13 14	3eqtr4g	|- ( ph -> X_ x e. A C = X_ y e. B D )