Definition df-mrex 35432

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 35412	. 2 class mREx
2		vt	. . 3 setvar 𝑡
3		cvv 3464	. . 3 class V
4	2	cv 1538	. . . . . 6 class 𝑡
5		cmcn 35406	. . . . . 6 class mCN
6	4, 5	cfv 6542	. . . . 5 class (mCN‘𝑡)
7		cmvar 35407	. . . . . 6 class mVR
8	4, 7	cfv 6542	. . . . 5 class (mVR‘𝑡)
9	6, 8	cun 3931	. . . 4 class ((mCN‘𝑡) ∪ (mVR‘𝑡))
10	9	cword 14535	. . 3 class Word ((mCN‘𝑡) ∪ (mVR‘𝑡))
11	2, 3, 10	cmpt 5207	. 2 class (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))
12	1, 11	wceq 1539	1 wff mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡)))

This definition is referenced by:  mrexval  35447