Metamath Proof Explorer

Definition df-mevl

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

Ref Expression
Assertion df-mevl 
|- mEval = Slot ; 2 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmevl 
 |-  mEval
1 c2 
 |-  2
2 cc0 
 |-  0
3 1 2 cdc 
 |-  ; 2 0
4 3 cslot 
 |-  Slot ; 2 0
5 0 4 wceq 
 |-  mEval = Slot ; 2 0