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 5886 and ovprc2 5887. 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 5854. (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 5850 | . 2 |
5 | 1, 2 | cop 3584 | . . 3 |
6 | 5, 3 | cfv 5196 | . 2 |
7 | 4, 6 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: oveq 5856 oveq1 5857 oveq2 5858 nfovd 5879 fnovex 5883 ovexg 5884 ovprc 5885 fnotovb 5893 ffnov 5954 eqfnov 5956 fnovim 5958 ovid 5966 ovidig 5967 ov 5969 ovigg 5970 ov6g 5987 ovg 5988 ovres 5989 fovrn 5992 fnrnov 5995 foov 5996 fnovrn 5997 funimassov 5999 ovelimab 6000 ovconst2 6001 elmpocl 6044 oprssdmm 6147 mpofvex 6179 oprab2co 6194 algrflem 6205 algrflemg 6206 mpoxopn0yelv 6215 ovtposg 6235 addpiord 7265 mulpiord 7266 addvalex 7793 cnref1o 9596 ioof 9915 frecuzrdgrrn 10351 frec2uzrdg 10352 frecuzrdgrcl 10353 frecuzrdgsuc 10357 frecuzrdgrclt 10358 frecuzrdgg 10359 frecuzrdgsuctlem 10366 seq3val 10401 seqvalcd 10402 cnrecnv 10861 eucalgval 11995 eucalginv 11997 eucalglt 11998 eucalg 12000 sqpweven 12116 2sqpwodd 12117 isstructim 12417 isstructr 12418 mgm1 12611 sgrp1 12638 mnd1 12666 mnd1id 12667 txdis1cn 13031 lmcn2 13033 cnmpt12f 13039 cnmpt21 13044 cnmpt2t 13046 cnmpt22 13047 psmetxrge0 13085 xmeterval 13188 comet 13252 txmetcnp 13271 qtopbasss 13274 cnmetdval 13282 remetdval 13292 tgqioo 13300 |
Copyright terms: Public domain | W3C validator |