Description: Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-msyn | ⊢ mSyn = Slot 6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmsy | ⊢ mSyn | |
1 | c6 | ⊢ 6 | |
2 | 1 | cslot | ⊢ Slot 6 |
3 | 0 2 | wceq | ⊢ mSyn = Slot 6 |