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