Metamath Proof Explorer

Definition df-mrex

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

Ref Expression
Assertion df-mrex 
|- mREx = ( t e. _V |-> Word ( ( mCN ` t ) u. ( mVR ` t ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrex 
 |-  mREx
1 vt 
 |-  t
2 cvv 
 |-  _V
3 cmcn 
 |-  mCN
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( mCN ` t )
6 cmvar 
 |-  mVR
7 4 6 cfv 
 |-  ( mVR ` t )
8 5 7 cun 
 |-  ( ( mCN ` t ) u. ( mVR ` t ) )
9 8 cword 
 |-  Word ( ( mCN ` t ) u. ( mVR ` t ) )
10 1 2 9 cmpt 
 |-  ( t e. _V |-> Word ( ( mCN ` t ) u. ( mVR ` t ) ) )
11 0 10 wceq 
 |-  mREx = ( t e. _V |-> Word ( ( mCN ` t ) u. ( mVR ` t ) ) )