Description: Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mevl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmevl | |
|
1 | c2 | |
|
2 | cc0 | |
|
3 | 1 2 | cdc | |
4 | 3 | cslot | |
5 | 0 4 | wceq | |