Metamath Proof Explorer

Definition df-msyn

Description: Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-msyn 
|- mSyn = Slot 6

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsy 
 |-  mSyn
1 c6 
 |-  6
2 1 cslot 
 |-  Slot 6
3 0 2 wceq 
 |-  mSyn = Slot 6