New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-ov | Unicode version |
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. This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when is a proper class. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5528. (Contributed by SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-ov |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | co 5525 | . 2 |
5 | 1, 2 | cop 4561 | . . 3 |
6 | 5, 3 | cfv 4781 | . 2 |
7 | 4, 6 | wceq 1642 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: oveq 5529 oveq1 5530 oveq2 5531 nfovd 5544 ovex 5551 fnopovb 5557 ffnov 5587 eqfnov 5589 fnov 5591 ovidig 5593 ov 5595 ovigg 5596 ov6g 5600 ovg 5601 ovres 5602 fovrn 5604 fnrnov 5605 foov 5606 fnovrn 5607 funimassov 5609 ovelimab 5610 ovconst2 5611 oprssdm 5612 ndmovg 5613 ndmovcl 5614 ndmov 5615 elovex12 5648 brcupg 5814 brcomposeg 5819 braddcfn 5826 brcrossg 5848 brfullfunop 5867 fce 6188 |
Copyright terms: Public domain | W3C validator |