Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mvt Structured version   Visualization version   Unicode version
Definition df-mvt 31382
Description: Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvt |- mVT = ( t e. _V |-> ran (mType ` t ) )
Detailed syntax breakdown of Definition df-mvt
StepHypRef Expression
1 cmvt 31360 . 2 class mVT
2 vt . . 3 setvar t
3 cvv 3200 . . 3 class _V
42cv 1482 . . . . 5 class t
5 cmty 31359 . . . . 5 class mType
64, 5cfv 5888 . . . 4 class (mType ` t )
76crn 5115 . . 3 class ran (mType ` t )
82, 3, 7cmpt 4729 . 2 class ( t e. _V |-> ran (mType ` t ) )
91, 8wceq 1483 1 wff mVT = ( t e. _V |-> ran (mType ` t ) )
Colors of variables: wff setvar class
This definition is referenced by:  mvtval  31397
  Copyright terms: Public domain W3C validator