df-mty - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-mty		Structured version Visualization version GIF version

Definition df-mty 35450

Description: Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)

**Assertion**
Ref	Expression
df-mty	⊢ mType = Slot 3

**Detailed syntax breakdown of Definition df-mty**
Step	Hyp	Ref	Expression
1		cmty 35430	. 2 class mType
2		c3 12294	. . 3 class 3
3	2	cslot 17198	. 2 class Slot 3
4	1, 3	wceq 1540	1 wff mType = Slot 3

Colors of variables: wff setvar class

This definition is referenced by: (None)