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  and its arguments  and
 - will be useful
for proving meaningful theorems. For example, if
class is the
operation  and
arguments and are 
and  , the expression
  can be proved to equal  (see
3p2e5 11160). This definition is well-defined, although
not very meaningful,
when classes
and/or are proper
classes (i.e. are not sets);
see ovprc1 6684 and ovprc2 6685. On the other hand, we often find uses for
this definition when is a proper class, such as  in oav 7591.
is normally
equal to a class of nested ordered pairs of the form
defined by df-oprab 6654. (Contributed by NM,
28-Feb-1995.) |
