![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ov | GIF 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 5924 and ovprc2 5925. 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 5892. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
df-ov | ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | co 5888 | . 2 class (𝐴𝐹𝐵) |
5 | 1, 2 | cop 3607 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cfv 5228 | . 2 class (𝐹‘〈𝐴, 𝐵〉) |
7 | 4, 6 | wceq 1363 | 1 wff (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
Colors of variables: wff set class |
This definition is referenced by: oveq 5894 oveq1 5895 oveq2 5896 nfovd 5917 fnovex 5921 ovexg 5922 ovprc 5923 fnotovb 5931 ffnov 5992 eqfnov 5994 fnovim 5996 ovid 6004 ovidig 6005 ov 6007 ovigg 6008 ov6g 6025 ovg 6026 ovres 6027 fovcdm 6030 fnrnov 6033 foov 6034 fnovrn 6035 funimassov 6037 ovelimab 6038 ovconst2 6039 elmpocl 6082 oprssdmm 6185 mpofvex 6217 oprab2co 6232 algrflem 6243 algrflemg 6244 mpoxopn0yelv 6253 ovtposg 6273 addpiord 7328 mulpiord 7329 addvalex 7856 cnref1o 9663 ioof 9984 frecuzrdgrrn 10421 frec2uzrdg 10422 frecuzrdgrcl 10423 frecuzrdgsuc 10427 frecuzrdgrclt 10428 frecuzrdgg 10429 frecuzrdgsuctlem 10436 seq3val 10471 seqvalcd 10472 cnrecnv 10932 eucalgval 12067 eucalginv 12069 eucalglt 12070 eucalg 12072 sqpweven 12188 2sqpwodd 12189 isstructim 12489 isstructr 12490 imasaddvallemg 12753 xpsff1o 12786 mgm1 12807 sgrp1 12835 mnd1 12868 mnd1id 12869 grp1 13002 srgfcl 13220 ring1 13304 txdis1cn 14049 lmcn2 14051 cnmpt12f 14057 cnmpt21 14062 cnmpt2t 14064 cnmpt22 14065 psmetxrge0 14103 xmeterval 14206 comet 14270 txmetcnp 14289 qtopbasss 14292 cnmetdval 14300 remetdval 14310 tgqioo 14318 |
Copyright terms: Public domain | W3C validator |