![]() |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-ov |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | co 5896 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3610 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | cfv 5235 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: oveq 5902 oveq1 5903 oveq2 5904 nfovd 5925 fnovex 5929 ovexg 5930 ovprc 5931 fnotovb 5939 ffnov 6000 eqfnov 6003 fnovim 6005 ovid 6013 ovidig 6014 ov 6016 ovigg 6017 ov6g 6034 ovg 6035 ovres 6036 fovcdm 6039 fnrnov 6042 foov 6043 fnovrn 6044 funimassov 6046 ovelimab 6047 ovconst2 6048 elmpocl 6091 oprssdmm 6196 mpofvex 6228 oprab2co 6243 algrflem 6254 algrflemg 6255 mpoxopn0yelv 6264 ovtposg 6284 addpiord 7345 mulpiord 7346 addvalex 7873 cnref1o 9680 ioof 10001 frecuzrdgrrn 10439 frec2uzrdg 10440 frecuzrdgrcl 10441 frecuzrdgsuc 10445 frecuzrdgrclt 10446 frecuzrdgg 10447 frecuzrdgsuctlem 10454 seq3val 10489 seqvalcd 10490 cnrecnv 10951 eucalgval 12086 eucalginv 12088 eucalglt 12089 eucalg 12091 sqpweven 12207 2sqpwodd 12208 isstructim 12526 isstructr 12527 relelbasov 12574 imasaddvallemg 12792 xpsff1o 12825 mgm1 12846 sgrp1 12874 mnd1 12907 mnd1id 12908 grp1 13050 srgfcl 13327 ring1 13411 txdis1cn 14235 lmcn2 14237 cnmpt12f 14243 cnmpt21 14248 cnmpt2t 14250 cnmpt22 14251 psmetxrge0 14289 xmeterval 14392 comet 14456 txmetcnp 14475 qtopbasss 14478 cnmetdval 14486 remetdval 14496 tgqioo 14504 |
Copyright terms: Public domain | W3C validator |