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=tVranmStRedt

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsta classmStat
1 vt setvart
2 cvv classV
3 cmsr classmStRed
4 1 cv setvart
5 4 3 cfv classmStRedt
6 5 crn classranmStRedt
7 1 2 6 cmpt classtVranmStRedt
8 0 7 wceq wffmStat=tVranmStRedt