Metamath Proof Explorer


Definition df-ov

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)

Ref Expression
Assertion df-ov A F B = F A B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cF class F
2 cB class B
3 0 2 1 co class A F B
4 0 2 cop class A B
5 4 1 cfv class F A B
6 3 5 wceq wff A F B = F A B