Metamath Proof Explorer

Definition df-msta

Description: Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-msta 
|- mStat = ( t e. _V |-> ran ( mStRed ` t ) )

Detailed syntax breakdown

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