Step |
Hyp |
Ref |
Expression |
1 |
|
dvhvscaval.s |
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) |
2 |
|
fveq1 |
|- ( s = t -> ( s ` ( 1st ` f ) ) = ( t ` ( 1st ` f ) ) ) |
3 |
|
coeq1 |
|- ( s = t -> ( s o. ( 2nd ` f ) ) = ( t o. ( 2nd ` f ) ) ) |
4 |
2 3
|
opeq12d |
|- ( s = t -> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. = <. ( t ` ( 1st ` f ) ) , ( t o. ( 2nd ` f ) ) >. ) |
5 |
|
2fveq3 |
|- ( f = g -> ( t ` ( 1st ` f ) ) = ( t ` ( 1st ` g ) ) ) |
6 |
|
fveq2 |
|- ( f = g -> ( 2nd ` f ) = ( 2nd ` g ) ) |
7 |
6
|
coeq2d |
|- ( f = g -> ( t o. ( 2nd ` f ) ) = ( t o. ( 2nd ` g ) ) ) |
8 |
5 7
|
opeq12d |
|- ( f = g -> <. ( t ` ( 1st ` f ) ) , ( t o. ( 2nd ` f ) ) >. = <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. ) |
9 |
4 8
|
cbvmpov |
|- ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. ) |
10 |
1 9
|
eqtri |
|- .x. = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. ) |