Metamath Proof Explorer

Definition df-mvt

Description: Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mvt 
|- mVT = ( t e. _V |-> ran ( mType ` t ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvt 
 |-  mVT
1 vt 
 |-  t
2 cvv 
 |-  _V
3 cmty 
 |-  mType
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( mType ` t )
6 5 crn 
 |-  ran ( mType ` t )
7 1 2 6 cmpt 
 |-  ( t e. _V |-> ran ( mType ` t ) )
8 0 7 wceq 
 |-  mVT = ( t e. _V |-> ran ( mType ` t ) )