| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cbvixpdavw.1 |
|- ( ( ph /\ x = y ) -> B = C ) |
| 2 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
| 3 |
2
|
adantl |
|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. A ) ) |
| 4 |
3
|
cbvabdavw |
|- ( ph -> { x | x e. A } = { y | y e. A } ) |
| 5 |
4
|
fneq2d |
|- ( ph -> ( t Fn { x | x e. A } <-> t Fn { y | y e. A } ) ) |
| 6 |
|
simpr |
|- ( ( ph /\ x = y ) -> x = y ) |
| 7 |
6
|
fveq2d |
|- ( ( ph /\ x = y ) -> ( t ` x ) = ( t ` y ) ) |
| 8 |
7 1
|
eleq12d |
|- ( ( ph /\ x = y ) -> ( ( t ` x ) e. B <-> ( t ` y ) e. C ) ) |
| 9 |
8
|
cbvraldva |
|- ( ph -> ( A. x e. A ( t ` x ) e. B <-> A. y e. A ( t ` y ) e. C ) ) |
| 10 |
5 9
|
anbi12d |
|- ( ph -> ( ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. B ) <-> ( t Fn { y | y e. A } /\ A. y e. A ( t ` y ) e. C ) ) ) |
| 11 |
10
|
abbidv |
|- ( ph -> { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. B ) } = { t | ( t Fn { y | y e. A } /\ A. y e. A ( t ` y ) e. C ) } ) |
| 12 |
|
df-ixp |
|- X_ x e. A B = { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. B ) } |
| 13 |
|
df-ixp |
|- X_ y e. A C = { t | ( t Fn { y | y e. A } /\ A. y e. A ( t ` y ) e. C ) } |
| 14 |
11 12 13
|
3eqtr4g |
|- ( ph -> X_ x e. A B = X_ y e. A C ) |