Theorem dvhvscacbv

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

	Ref	Expression
Hypothesis	dvhvscaval.s	$$⊢\underset{\dot{}}{·}=\left(s\in E,f\in \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)$$
Assertion	dvhvscacbv	$$⊢\underset{\dot{}}{·}=\left(t\in E,g\in \left(T\times E\right)⟼⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvhvscaval.s	$$⊢\underset{\dot{}}{·}=\left(s\in E,f\in \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)$$
2		fveq1	$$⊢s=t\to s\left(1^{st}\left(f\right)\right)=t\left(1^{st}\left(f\right)\right)$$
3		coeq1	$$⊢s=t\to s\circ 2^{nd}\left(f\right)=t\circ 2^{nd}\left(f\right)$$
4	2 3	opeq12d	$$⊢s=t\to ⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩=⟨t\left(1^{st}\left(f\right)\right),t\circ 2^{nd}\left(f\right)⟩$$
5		2fveq3	$$⊢f=g\to t\left(1^{st}\left(f\right)\right)=t\left(1^{st}\left(g\right)\right)$$
6		fveq2	$$⊢f=g\to 2^{nd}\left(f\right)=2^{nd}\left(g\right)$$
7	6	coeq2d	$$⊢f=g\to t\circ 2^{nd}\left(f\right)=t\circ 2^{nd}\left(g\right)$$
8	5 7	opeq12d	$$⊢f=g\to ⟨t\left(1^{st}\left(f\right)\right),t\circ 2^{nd}\left(f\right)⟩=⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩$$
9	4 8	cbvmpov	$$⊢\left(s\in E,f\in \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)=\left(t\in E,g\in \left(T\times E\right)⟼⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩\right)$$
10	1 9	eqtri	$$⊢\underset{\dot{}}{·}=\left(t\in E,g\in \left(T\times E\right)⟼⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩\right)$$