# 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$