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