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