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 = ( mVR ` T )
	mvhfval.y	|- Y = ( mType ` T )
	mvhfval.h	|- H = ( mVH ` T )
Assertion	mvhval	|- ( X e. V -> ( H ` X ) = <. ( Y ` X ) , <" X "> >. )

Proof

Step	Hyp	Ref	Expression
1		mvhfval.v	|- V = ( mVR ` T )
2		mvhfval.y	|- Y = ( mType ` T )
3		mvhfval.h	|- H = ( mVH ` T )
4		fveq2	|- ( v = X -> ( Y ` v ) = ( Y ` X ) )
5		s1eq	|- ( v = X -> <" v "> = <" X "> )
6	4 5	opeq12d	|- ( v = X -> <. ( Y ` v ) , <" v "> >. = <. ( Y ` X ) , <" X "> >. )
7	1 2 3	mvhfval	|- H = ( v e. V |-> <. ( Y ` v ) , <" v "> >. )
8		opex	|- <. ( Y ` X ) , <" X "> >. e. _V
9	6 7 8	fvmpt	|- ( X e. V -> ( H ` X ) = <. ( Y ` X ) , <" X "> >. )