# 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
` |-  A`
1 cF
` |-  F`
2 cB
` |-  B`
3 0 2 1 co
` |-  ( A F B )`
4 0 2 cop
` |-  <. A , B >.`
5 4 1 cfv
` |-  ( F ` <. A , B >. )`
6 3 5 wceq
` |-  ( A F B ) = ( F ` <. A , B >. )`