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

Metamath Proof Explorer

Theorem dvhvscacbv

Description: Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013)

Ref Expression
Hypothesis dvhvscaval.s 
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
Assertion dvhvscacbv 
|- .x. = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. )

Proof

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 ) ) >. )