Definition df-mrex 32735

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 32715	. 2 class mREx
2		vt	. . 3 setvar 𝑡
3		cvv 3496	. . 3 class V
4	2	cv 1536	. . . . . 6 class 𝑡
5		cmcn 32709	. . . . . 6 class mCN
6	4, 5	cfv 6357	. . . . 5 class (mCN‘𝑡)
7		cmvar 32710	. . . . . 6 class mVR
8	4, 7	cfv 6357	. . . . 5 class (mVR‘𝑡)
9	6, 8	cun 3936	. . . 4 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
10	9	cword 13864	. . 3 class Word ((mCN‘𝑡) ∪ (mVR‘𝑡))
11	2, 3, 10	cmpt 5148	. 2 class (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))
12	1, 11	wceq 1537	1 wff mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))

This definition is referenced by:  mrexval  32750