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 9408 ioof 9722 frecuzrdgrrn 10149 frec2uzrdg 10150 frecuzrdgrcl 10151 frecuzrdgsuc 10155 frecuzrdgrclt 10156 frecuzrdgg 10157 frecuzrdgsuctlem 10164 seq3val 10199 seqvalcd 10200 cnrecnv 10650 eucalgval 11662 eucalginv 11664 eucalglt 11665 eucalg 11667 sqpweven 11780 2sqpwodd 11781 isstructim 11900 isstructr 11901 txdis1cn 12374 lmcn2 12376 cnmpt12f 12382 cnmpt21 12387 cnmpt2t 12389 cnmpt22 12390 psmetxrge0 12428 xmeterval 12531 comet 12595 txmetcnp 12614 qtopbasss 12617 cnmetdval 12625 remetdval 12635 tgqioo 12643 |
Copyright terms: Public domain | W3C validator |