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 class mSyn
1 c6 class 6
2 1 cslot class Slot 6
3 0 2 wceq wff mSyn = Slot 6