Definition df-mvh

Description: Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvh	|- mVH = ( t e. _V |-> ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvh	|- mVH
1		vt	|- t
2		cvv	|- _V
3		vv	|- v
4		cmvar	|- mVR
5	1	cv	|- t
6	5 4	cfv	|- ( mVR ` t )
7		cmty	|- mType
8	5 7	cfv	|- ( mType ` t )
9	3	cv	|- v
10	9 8	cfv	|- ( ( mType ` t ) ` v )
11	9	cs1	|- <" v ">
12	10 11	cop	|- <. ( ( mType ` t ) ` v ) , <" v "> >.
13	3 6 12	cmpt	|- ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. )
14	1 2 13	cmpt	|- ( t e. _V |-> ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. ) )
15	0 14	wceq	|- mVH = ( t e. _V |-> ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. ) )