# Metamath Proof Explorer

## 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 ${setvar}{t}$
2 cvv ${class}\mathrm{V}$
3 cmcn ${class}\mathrm{mCN}$
4 1 cv ${setvar}{t}$
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)$