Definition df-mrex 31383

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 = ( t e. _V |-> Word ( (mCN ` t ) u. (mVR ` t ) ) )

Detailed syntax breakdown of Definition df-mrex

Step	Hyp	Ref	Expression
1		cmrex 31363	. 2 class mREx
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . 6 class t
5		cmcn 31357	. . . . . 6 class mCN
6	4, 5	cfv 5888	. . . . 5 class (mCN ` t )
7		cmvar 31358	. . . . . 6 class mVR
8	4, 7	cfv 5888	. . . . 5 class (mVR ` t )
9	6, 8	cun 3572	. . . 4 class ( (mCN ` t ) u. (mVR ` t ) )
10	9	cword 13291	. . 3 class Word ( (mCN ` t ) u. (mVR ` t ) )
11	2, 3, 10	cmpt 4729	. 2 class ( t e. _V |-> Word ( (mCN ` t ) u. (mVR ` t ) ) )
12	1, 11	wceq 1483	1 wff mREx = ( t e. _V |-> Word ( (mCN ` t ) u. (mVR ` t ) ) )

This definition is referenced by:  mrexval  31398