Definition df-mex

Description: Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mex	⊢ mEx = ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmex	⊢ mEx
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmtc	⊢ mTC
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mTC ‘ 𝑡 )
6		cmrex	⊢ mREx
7	4 6	cfv	⊢ ( mREx ‘ 𝑡 )
8	5 7	cxp	⊢ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) )
9	1 2 8	cmpt	⊢ ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )
10	0 9	wceq	⊢ mEx = ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )