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