Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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. For example, if class is the operation + and arguments and are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets); see ovprc1 5775 and ovprc2 5776. 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 5746. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
df-ov |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | co 5742 | . 2 |
5 | 1, 2 | cop 3500 | . . 3 |
6 | 5, 3 | cfv 5093 | . 2 |
7 | 4, 6 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: oveq 5748 oveq1 5749 oveq2 5750 nfovd 5768 fnovex 5772 ovexg 5773 ovprc 5774 fnotovb 5782 ffnov 5843 eqfnov 5845 fnovim 5847 ovid 5855 ovidig 5856 ov 5858 ovigg 5859 ov6g 5876 ovg 5877 ovres 5878 fovrn 5881 fnrnov 5884 foov 5885 fnovrn 5886 funimassov 5888 ovelimab 5889 ovconst2 5890 elmpocl 5936 oprssdmm 6037 mpofvex 6069 oprab2co 6083 algrflem 6094 algrflemg 6095 mpoxopn0yelv 6104 ovtposg 6124 addpiord 7092 mulpiord 7093 addvalex 7620 cnref1o 9396 ioof 9709 frecuzrdgrrn 10136 frec2uzrdg 10137 frecuzrdgrcl 10138 frecuzrdgsuc 10142 frecuzrdgrclt 10143 frecuzrdgg 10144 frecuzrdgsuctlem 10151 seq3val 10186 seqvalcd 10187 cnrecnv 10637 eucalgval 11647 eucalginv 11649 eucalglt 11650 eucalg 11652 sqpweven 11764 2sqpwodd 11765 isstructim 11884 isstructr 11885 txdis1cn 12358 lmcn2 12360 cnmpt12f 12366 cnmpt21 12371 cnmpt2t 12373 cnmpt22 12374 psmetxrge0 12412 xmeterval 12515 comet 12579 txmetcnp 12598 qtopbasss 12601 cnmetdval 12609 remetdval 12619 tgqioo 12627 |
Copyright terms: Public domain | W3C validator |