Definition df-muv

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

	Ref	Expression
Assertion	df-muv	⊢ mUV = Slot 7

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmuv	⊢ mUV
1		c7	⊢ 7
2	1	cslot	⊢ Slot 7
3	0 2	wceq	⊢ mUV = Slot 7