Definition df-mrex 30637

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 30617	. 2 class mREx
2		vt	. . 3 setvar 𝑡
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . . 6 class 𝑡
5		cmcn 30611	. . . . . 6 class mCN
6	4, 5	cfv 5804	. . . . 5 class (mCN‘𝑡)
7		cmvar 30612	. . . . . 6 class mVR
8	4, 7	cfv 5804	. . . . 5 class (mVR‘𝑡)
9	6, 8	cun 3538	. . . 4 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
10	9	cword 13146	. . 3 class Word ((mCN‘𝑡) ∪ (mVR‘𝑡))
11	2, 3, 10	cmpt 4643	. 2 class (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))
12	1, 11	wceq 1475	1 wff mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))

This definition is referenced by:  mrexval  30652