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	$$⊢\mathrm{mEx}=\left(t\in \mathrm{V}⟼\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmex	$$class\mathrm{mEx}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmtc	$$class\mathrm{mTC}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mTC}\left(t\right)$$
6		cmrex	$$class\mathrm{mREx}$$
7	4 6	cfv	$$class\mathrm{mREx}\left(t\right)$$
8	5 7	cxp	$$class\left(\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\right)$$
9	1 2 8	cmpt	$$class\left(t\in \mathrm{V}⟼\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\right)$$
10	0 9	wceq	$$wff\mathrm{mEx}=\left(t\in \mathrm{V}⟼\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\right)$$