Metamath Proof Explorer

Definition df-mvar

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

Ref Expression
Assertion df-mvar 
|- mVR = Slot 2

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvar 
 |-  mVR
1 c2 
 |-  2
2 1 cslot 
 |-  Slot 2
3 0 2 wceq 
 |-  mVR = Slot 2