Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-msta Structured version   Visualization version   Unicode version
Definition df-msta 31392
Description: Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-msta |- mStat = ( t e. _V |-> ran (mStRed ` t ) )
Detailed syntax breakdown of Definition df-msta
StepHypRef Expression
1 cmsta 31372 . 2 class mStat
2 vt . . 3 setvar t
3 cvv 3200 . . 3 class _V
42cv 1482 . . . . 5 class t
5 cmsr 31371 . . . . 5 class mStRed
64, 5cfv 5888 . . . 4 class (mStRed ` t )
76crn 5115 . . 3 class ran (mStRed ` t )
82, 3, 7cmpt 4729 . 2 class ( t e. _V |-> ran (mStRed ` t ) )
91, 8wceq 1483 1 wff mStat = ( t e. _V |-> ran (mStRed ` t ) )
Colors of variables: wff setvar class
This definition is referenced by:  mstaval  31441
  Copyright terms: Public domain W3C validator