# 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`