Description: Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mty | ⊢ mType = Slot 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmty | ⊢ mType | |
1 | c3 | ⊢ 3 | |
2 | 1 | cslot | ⊢ Slot 3 |
3 | 0 2 | wceq | ⊢ mType = Slot 3 |