Theorem cbvixp

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011)

	Ref	Expression
Hypotheses	cbvixp.1	|- F/_ y B
	cbvixp.2	|- F/_ x C
	cbvixp.3	|- ( x = y -> B = C )
Assertion	cbvixp	|- X_ x e. A B = X_ y e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvixp.1	|- F/_ y B
2		cbvixp.2	|- F/_ x C
3		cbvixp.3	|- ( x = y -> B = C )
4	1	nfel2	|- F/ y ( f ` x ) e. B
5	2	nfel2	|- F/ x ( f ` y ) e. C
6		fveq2	|- ( x = y -> ( f ` x ) = ( f ` y ) )
7	6 3	eleq12d	|- ( x = y -> ( ( f ` x ) e. B <-> ( f ` y ) e. C ) )
8	4 5 7	cbvralw	|- ( A. x e. A ( f ` x ) e. B <-> A. y e. A ( f ` y ) e. C )
9	8	anbi2i	|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> ( f Fn A /\ A. y e. A ( f ` y ) e. C ) )
10	9	abbii	|- { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) } = { f | ( f Fn A /\ A. y e. A ( f ` y ) e. C ) }
11		dfixp	|- X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }
12		dfixp	|- X_ y e. A C = { f | ( f Fn A /\ A. y e. A ( f ` y ) e. C ) }
13	10 11 12	3eqtr4i	|- X_ x e. A B = X_ y e. A C