Definition df-mex 31384

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 = ( t e. _V |-> ( (mTC ` t ) X. (mREx ` t ) ) )

Detailed syntax breakdown of Definition df-mex

Step	Hyp	Ref	Expression
1		cmex 31364	. 2 class mEx
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class t
5		cmtc 31361	. . . . 5 class mTC
6	4, 5	cfv 5888	. . . 4 class (mTC ` t )
7		cmrex 31363	. . . . 5 class mREx
8	4, 7	cfv 5888	. . . 4 class (mREx ` t )
9	6, 8	cxp 5112	. . 3 class ( (mTC ` t ) X. (mREx ` t ) )
10	2, 3, 9	cmpt 4729	. 2 class ( t e. _V |-> ( (mTC ` t ) X. (mREx ` t ) ) )
11	1, 10	wceq 1483	1 wff mEx = ( t e. _V |-> ( (mTC ` t ) X. (mREx ` t ) ) )

This definition is referenced by:  mexval  31399