Definition df-mrex

Description: Define the set of "raw expressions", which are expressions without a typecode attached. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mrex	$$⊢\mathrm{mREx}=\left(t\in \mathrm{V}⟼\mathrm{Word}\left(\mathrm{mCN}\left(t\right)\cup \mathrm{mVR}\left(t\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmrex	$$class\mathrm{mREx}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmcn	$$class\mathrm{mCN}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mCN}\left(t\right)$$
6		cmvar	$$class\mathrm{mVR}$$
7	4 6	cfv	$$class\mathrm{mVR}\left(t\right)$$
8	5 7	cun	$$class\left(\mathrm{mCN}\left(t\right)\cup \mathrm{mVR}\left(t\right)\right)$$
9	8	cword	$$class\mathrm{Word}\left(\mathrm{mCN}\left(t\right)\cup \mathrm{mVR}\left(t\right)\right)$$
10	1 2 9	cmpt	$$class\left(t\in \mathrm{V}⟼\mathrm{Word}\left(\mathrm{mCN}\left(t\right)\cup \mathrm{mVR}\left(t\right)\right)\right)$$
11	0 10	wceq	$$wff\mathrm{mREx}=\left(t\in \mathrm{V}⟼\mathrm{Word}\left(\mathrm{mCN}\left(t\right)\cup \mathrm{mVR}\left(t\right)\right)\right)$$