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

Metamath Proof Explorer

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