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	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mvhfval.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
	mvhfval.h	$$⊢H=\mathrm{mVH}\left(T\right)$$
Assertion	mvhval	$$⊢X\in V\to H\left(X\right)=⟨Y\left(X\right),⟨“X”⟩⟩$$

Proof

Step	Hyp	Ref	Expression
1		mvhfval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mvhfval.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
3		mvhfval.h	$$⊢H=\mathrm{mVH}\left(T\right)$$
4		fveq2	$$⊢v=X\to Y\left(v\right)=Y\left(X\right)$$
5		s1eq	$$⊢v=X\to ⟨“v”⟩=⟨“X”⟩$$
6	4 5	opeq12d	$$⊢v=X\to ⟨Y\left(v\right),⟨“v”⟩⟩=⟨Y\left(X\right),⟨“X”⟩⟩$$
7	1 2 3	mvhfval	$$⊢H=\left(v\in V⟼⟨Y\left(v\right),⟨“v”⟩⟩\right)$$
8		opex	$$⊢⟨Y\left(X\right),⟨“X”⟩⟩\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢X\in V\to H\left(X\right)=⟨Y\left(X\right),⟨“X”⟩⟩$$