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=Slot6

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsy classmSyn
1 c6 class6
2 1 cslot classSlot6
3 0 2 wceq wffmSyn=Slot6