Metamath Proof Explorer

Definition df-mty

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmty 
 |-  mType
1 c3 
 |-  3
2 1 cslot 
 |-  Slot 3
3 0 2 wceq 
 |-  mType = Slot 3