Metamath Proof Explorer


Theorem dvhvscacbv

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

Ref Expression
Hypothesis dvhvscaval.s · ˙ = s E , f T × E s 1 st f s 2 nd f
Assertion dvhvscacbv · ˙ = t E , g T × E t 1 st g t 2 nd g

Proof

Step Hyp Ref Expression
1 dvhvscaval.s · ˙ = s E , f T × E s 1 st f s 2 nd f
2 fveq1 s = t s 1 st f = t 1 st f
3 coeq1 s = t s 2 nd f = t 2 nd f
4 2 3 opeq12d s = t s 1 st f s 2 nd f = t 1 st f t 2 nd f
5 2fveq3 f = g t 1 st f = t 1 st g
6 fveq2 f = g 2 nd f = 2 nd g
7 6 coeq2d f = g t 2 nd f = t 2 nd g
8 5 7 opeq12d f = g t 1 st f t 2 nd f = t 1 st g t 2 nd g
9 4 8 cbvmpov s E , f T × E s 1 st f s 2 nd f = t E , g T × E t 1 st g t 2 nd g
10 1 9 eqtri · ˙ = t E , g T × E t 1 st g t 2 nd g