Metamath Proof Explorer


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 class mUV
1 c7 class 7
2 1 cslot class Slot 7
3 0 2 wceq wff mUV = Slot 7