Definition df-mvt

Description: Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvt	$$⊢\mathrm{mVT}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mType}\left(t\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvt	$$class\mathrm{mVT}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmty	$$class\mathrm{mType}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mType}\left(t\right)$$
6	5	crn	$$class\mathrm{ran}\mathrm{mType}\left(t\right)$$
7	1 2 6	cmpt	$$class\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mType}\left(t\right)\right)$$
8	0 7	wceq	$$wff\mathrm{mVT}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mType}\left(t\right)\right)$$