# 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 ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cF 𝐹
2 cB 𝐵
3 0 2 1 co ( 𝐴 𝐹 𝐵 )
4 0 2 cop 𝐴 , 𝐵
5 4 1 cfv ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 3 5 wceq ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )