Metamath Proof Explorer


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 mVH = t V v mVR t mType t v ⟨“ v ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvh class mVH
1 vt setvar t
2 cvv class V
3 vv setvar v
4 cmvar class mVR
5 1 cv setvar t
6 5 4 cfv class mVR t
7 cmty class mType
8 5 7 cfv class mType t
9 3 cv setvar v
10 9 8 cfv class mType t v
11 9 cs1 class ⟨“ v ”⟩
12 10 11 cop class mType t v ⟨“ v ”⟩
13 3 6 12 cmpt class v mVR t mType t v ⟨“ v ”⟩
14 1 2 13 cmpt class t V v mVR t mType t v ⟨“ v ”⟩
15 0 14 wceq wff mVH = t V v mVR t mType t v ⟨“ v ”⟩