Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Models of formal systems
df-mevl
Next ⟩
df-mvl
Metamath Proof Explorer
Ascii
Unicode
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
9
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmevl
class
mEval
1
c9
class
9
2
1
cslot
class
Slot
9
3
0
2
wceq
wff
mEval
=
Slot
9