Definition df-mvh 31389

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

Assertion

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

Distinct variable group:   v, t

Detailed syntax breakdown of Definition df-mvh

Step	Hyp	Ref	Expression
1		cmvh 31369	. 2 class mVH
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1482	. . . . 5 class t
6		cmvar 31358	. . . . 5 class mVR
7	5, 6	cfv 5888	. . . 4 class (mVR ` t )
8	4	cv 1482	. . . . . 6 class v
9		cmty 31359	. . . . . . 7 class mType
10	5, 9	cfv 5888	. . . . . 6 class (mType ` t )
11	8, 10	cfv 5888	. . . . 5 class ( (mType ` t ) ` v )
12	8	cs1 13294	. . . . 5 class <" v ">
13	11, 12	cop 4183	. . . 4 class <. ( (mType ` t ) ` v ) , <" v "> >.
14	4, 7, 13	cmpt 4729	. . 3 class ( v e. (mVR ` t ) |-> <. ( (mType ` t ) ` v ) , <" v "> >. )
15	2, 3, 14	cmpt 4729	. 2 class ( t e. _V |-> ( v e. (mVR ` t ) |-> <. ( (mType ` t ) ` v ) , <" v "> >. ) )
16	1, 15	wceq 1483	1 wff mVH = ( t e. _V |-> ( v e. (mVR ` t ) |-> <. ( (mType ` t ) ` v ) , <" v "> >. ) )

This definition is referenced by:  mvhfval  31430