This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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