Description: Define the value of an operation. Definition of operation value in
Enderton p. 79. Note that the syntax is simply three class expressions
in a row bracketed by parentheses. There are no restrictions of any kind
on what those class expressions may be, although only certain kinds of
class expressions - a binary operation F and its arguments A and
B - will be useful for proving meaningful theorems. For example, if
class F is the operation + and arguments A and B are 3
and 2 , the expression ( 3 + 2 ) can be proved to equal 5 (see
3p2e5 ). This definition is well-defined, although not very meaningful,
when classes A and/or B are proper classes (i.e. are not sets);
see ovprc1 and ovprc2 . On the other hand, we often find uses for
this definition when F is a proper class, such as +o in oav .
F is normally equal to a class of nested ordered pairs of the form
defined by df-oprab . (Contributed by NM, 28-Feb-1995)