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

Definition df-ov 5713
 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 and , the expression can be proved to equal (see 3p2e5 9734). This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets); see ovprc1 5738 and ovprc2 5739. On the other hand, we often find uses for this definition when is a proper class, such as in oav 6396. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5714. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3
41, 2, 3co 5710 . 2
51, 2cop 3547 . . 3
65, 3cfv 4592 . 2
74, 6wceq 1619 1