Metamath Proof Explorer
Table of Contents - 20.16.5.18. Evaluation
This section treats the existing predicate (df-slot) as
"evaluation at a class" and for the moment does not introduce new syntax for
it.
- bj-evaleq
- bj-evalfun
- bj-evalfn
- bj-evalval
- bj-evalid
- bj-ndxarg
- bj-evalidval