dvhvscacbv

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

		Ref	Expression
	Hypothesis	dvhvscaval.s	⊢ · = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
	Assertion	dvhvscacbv	⊢ · = ( 𝑡 ∈ 𝐸 , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )

Step	Hyp	Ref	Expression
1		dvhvscaval.s	⊢ · = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
2		fveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) = ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) )
3		coeq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) )
4	2 3	opeq12d	⊢ ( 𝑠 = 𝑡 → ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
5		2fveq3	⊢ ( 𝑓 = 𝑔 → ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) = ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) )
6		fveq2	⊢ ( 𝑓 = 𝑔 → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝑔 ) )
7	6	coeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) )
8	5 7	opeq12d	⊢ ( 𝑓 = 𝑔 → ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )
9	4 8	cbvmpov	⊢ ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑡 ∈ 𝐸 , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )
10	1 9	eqtri	⊢ · = ( 𝑡 ∈ 𝐸 , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )

Metamath Proof Explorer