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