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 = ( 𝑡 ∈ V ↦ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmrex	⊢ mREx
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmcn	⊢ mCN
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mCN ‘ 𝑡 )
6		cmvar	⊢ mVR
7	4 6	cfv	⊢ ( mVR ‘ 𝑡 )
8	5 7	cun	⊢ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) )
9	8	cword	⊢ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) )
10	1 2 9	cmpt	⊢ ( 𝑡 ∈ V ↦ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) )
11	0 10	wceq	⊢ mREx = ( 𝑡 ∈ V ↦ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) )