Metamath Proof Explorer

Table of Contents - 21.20.5.19. Evaluation at a class

This section treats the existing predicate (df-slot) as "evaluation at a class" and for the moment does not introduce new syntax for it.

1. bj-evaleq
2. bj-evalfun
3. bj-evalfn
4. bj-evalval
5. bj-evalid
6. bj-ndxarg
7. bj-evalidval