Definition df-mvh

Description: Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvh	$$⊢\mathrm{mVH}=\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mVR}\left(t\right)⟼⟨\mathrm{mType}\left(t\right)\left(v\right),⟨“v”⟩⟩\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvh	$$class\mathrm{mVH}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vv	$$setvarv$$
4		cmvar	$$class\mathrm{mVR}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mVR}\left(t\right)$$
7		cmty	$$class\mathrm{mType}$$
8	5 7	cfv	$$class\mathrm{mType}\left(t\right)$$
9	3	cv	$$setvarv$$
10	9 8	cfv	$$class\mathrm{mType}\left(t\right)\left(v\right)$$
11	9	cs1	$$class⟨“v”⟩$$
12	10 11	cop	$$class⟨\mathrm{mType}\left(t\right)\left(v\right),⟨“v”⟩⟩$$
13	3 6 12	cmpt	$$class\left(v\in \mathrm{mVR}\left(t\right)⟼⟨\mathrm{mType}\left(t\right)\left(v\right),⟨“v”⟩⟩\right)$$
14	1 2 13	cmpt	$$class\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mVR}\left(t\right)⟼⟨\mathrm{mType}\left(t\right)\left(v\right),⟨“v”⟩⟩\right)\right)$$
15	0 14	wceq	$$wff\mathrm{mVH}=\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mVR}\left(t\right)⟼⟨\mathrm{mType}\left(t\right)\left(v\right),⟨“v”⟩⟩\right)\right)$$