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=Slot20

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmevl classmEval
1 c2 class2
2 cc0 class0
3 1 2 cdc class20
4 3 cslot classSlot20
5 0 4 wceq wffmEval=Slot20