Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mvh Structured version   Unicode version

Definition df-mvh 29918
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
StepHypRef Expression
1 cmvh 29898 . 2  class mVH
2 vt . . 3  setvar  t
3 cvv 3087 . . 3  class  _V
4 vv . . . 4  setvar  v
52cv 1436 . . . . 5  class  t
6 cmvar 29887 . . . . 5  class mVR
75, 6cfv 5601 . . . 4  class  (mVR `  t )
84cv 1436 . . . . . 6  class  v
9 cmty 29888 . . . . . . 7  class mType
105, 9cfv 5601 . . . . . 6  class  (mType `  t )
118, 10cfv 5601 . . . . 5  class  ( (mType `  t ) `  v
)
128cs1 12646 . . . . 5  class  <" v ">
1311, 12cop 4008 . . . 4  class  <. (
(mType `  t ) `  v ) ,  <" v "> >.
144, 7, 13cmpt 4484 . . 3  class  ( v  e.  (mVR `  t
)  |->  <. ( (mType `  t ) `  v
) ,  <" v "> >. )
152, 3, 14cmpt 4484 . 2  class  ( t  e.  _V  |->  ( v  e.  (mVR `  t
)  |->  <. ( (mType `  t ) `  v
) ,  <" v "> >. ) )
161, 15wceq 1437 1  wff mVH  =  ( t  e.  _V  |->  ( v  e.  (mVR `  t )  |->  <. (
(mType `  t ) `  v ) ,  <" v "> >. )
)
Colors of variables: wff setvar class
This definition is referenced by:  mvhfval  29959
  Copyright terms: Public domain W3C validator