Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Grammatical formal systems
df-msyn
Next ⟩
df-mesyn
Metamath Proof Explorer
Ascii
Structured
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