Description: Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mtc | |- mTC = Slot 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmtc | |- mTC |
|
1 | c4 | |- 4 |
|
2 | 1 | cslot | |- Slot 4 |
3 | 0 2 | wceq | |- mTC = Slot 4 |