Definition df-msta

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

	Ref	Expression
Assertion	df-msta	$$⊢\mathrm{mStat}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mStRed}\left(t\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsta	$$class\mathrm{mStat}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmsr	$$class\mathrm{mStRed}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mStRed}\left(t\right)$$
6	5	crn	$$class\mathrm{ran}\mathrm{mStRed}\left(t\right)$$
7	1 2 6	cmpt	$$class\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mStRed}\left(t\right)\right)$$
8	0 7	wceq	$$wff\mathrm{mStat}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mStRed}\left(t\right)\right)$$