Definition df-muv

Description: Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-muv	$$⊢\mathrm{mUV}=\mathrm{Slot}7$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmuv	$$class\mathrm{mUV}$$
1		c7	$$class7$$
2	1	cslot	$$class\mathrm{Slot}7$$
3	0 2	wceq	$$wff\mathrm{mUV}=\mathrm{Slot}7$$