Definition df-mrex 36067

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

Assertion

Ref	Expression
df-mrex	⊢ mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))

Detailed syntax breakdown of Definition df-mrex

Step	Hyp	Ref	Expression
1		cmrex 36047	. 2 class mREx
2		vt	. . 3 setvar 𝑡
3		cvv 3453	. . 3 class V
4	2	cv 1569	. . . . . 6 class 𝑡
5		cmcn 36041	. . . . . 6 class mCN
6	4, 5	cfv 6537	. . . . 5 class (mCN‘𝑡)
7		cmvar 36042	. . . . . 6 class mVR
8	4, 7	cfv 6537	. . . . 5 class (mVR‘𝑡)
9	6, 8	cun 3900	. . . 4 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
10	9	cword 14580	. . 3 class Word ((mCN‘𝑡) ∪ (mVR‘𝑡))
11	2, 3, 10	cmpt 5190	. 2 class (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))
12	1, 11	wceq 1570	1 wff mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))

This definition is used by:  mrexval  36082