Theorem cbvixpdavw

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

	Ref	Expression
Hypothesis	cbvixpdavw.1	|- ( ( ph /\ x = y ) -> B = C )
Assertion	cbvixpdavw	|- ( ph -> X_ x e. A B = X_ y e. A C )

Proof

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