dvhvscacbv

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

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

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

Metamath Proof Explorer