Theorem mvhval

Description: Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvhfval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvhfval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
	mvhfval.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	mvhval	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐻 ‘ 𝑋 ) = ⟨ ( 𝑌 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		mvhfval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvhfval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
3		mvhfval.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
4		fveq2	⊢ ( 𝑣 = 𝑋 → ( 𝑌 ‘ 𝑣 ) = ( 𝑌 ‘ 𝑋 ) )
5		s1eq	⊢ ( 𝑣 = 𝑋 → ⟨“ 𝑣 ”⟩ = ⟨“ 𝑋 ”⟩ )
6	4 5	opeq12d	⊢ ( 𝑣 = 𝑋 → ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( 𝑌 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ⟩ )
7	1 2 3	mvhfval	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
8		opex	⊢ ⟨ ( 𝑌 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ⟩ ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐻 ‘ 𝑋 ) = ⟨ ( 𝑌 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ⟩ )