Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ov Structured version   Visualization version   GIF version

Definition df-ov 6804
 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 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 11323). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6835 and ovprc2 6836. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7748. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6805. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3co 6801 . 2 class (𝐴𝐹𝐵)
51, 2cop 4315 . . 3 class 𝐴, 𝐵
65, 3cfv 6037 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1620 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)