Definition df-mex 30638

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.)

Assertion

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

Detailed syntax breakdown of Definition df-mex

Step	Hyp	Ref	Expression
1		cmex 30618	. 2 class mEx
2		vt	. . 3 setvar 𝑡
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . 5 class 𝑡
5		cmtc 30615	. . . . 5 class mTC
6	4, 5	cfv 5804	. . . 4 class (mTC‘𝑡)
7		cmrex 30617	. . . . 5 class mREx
8	4, 7	cfv 5804	. . . 4 class (mREx‘𝑡)
9	6, 8	cxp 5036	. . 3 class ((mTC‘𝑡) × (mREx‘𝑡))
10	2, 3, 9	cmpt 4643	. 2 class (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
11	1, 10	wceq 1475	1 wff mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))

This definition is referenced by:  mexval  30653