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 -> B = C )
Assertion	cbvixpv	|- X_ x e. A B = X_ y e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvixpv.1	|- ( x = y -> B = C )
2		fveq2	|- ( x = y -> ( z ` x ) = ( z ` y ) )
3	2 1	eleq12d	|- ( x = y -> ( ( z ` x ) e. B <-> ( z ` y ) e. C ) )
4	3	cbvralvw	|- ( A. x e. A ( z ` x ) e. B <-> A. y e. A ( z ` y ) e. C )
5	4	anbi2i	|- ( ( z Fn A /\ A. x e. A ( z ` x ) e. B ) <-> ( z Fn A /\ A. y e. A ( z ` y ) e. C ) )
6	5	abbii	|- { z | ( z Fn A /\ A. x e. A ( z ` x ) e. B ) } = { z | ( z Fn A /\ A. y e. A ( z ` y ) e. C ) }
7		dfixp	|- X_ x e. A B = { z | ( z Fn A /\ A. x e. A ( z ` x ) e. B ) }
8		dfixp	|- X_ y e. A C = { z | ( z Fn A /\ A. y e. A ( z ` y ) e. C ) }
9	6 7 8	3eqtr4i	|- X_ x e. A B = X_ y e. A C