![]() |
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 5782 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3535 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | cfv 5131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1332 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: oveq 5788 oveq1 5789 oveq2 5790 nfovd 5808 fnovex 5812 ovexg 5813 ovprc 5814 fnotovb 5822 ffnov 5883 eqfnov 5885 fnovim 5887 ovid 5895 ovidig 5896 ov 5898 ovigg 5899 ov6g 5916 ovg 5917 ovres 5918 fovrn 5921 fnrnov 5924 foov 5925 fnovrn 5926 funimassov 5928 ovelimab 5929 ovconst2 5930 elmpocl 5976 oprssdmm 6077 mpofvex 6109 oprab2co 6123 algrflem 6134 algrflemg 6135 mpoxopn0yelv 6144 ovtposg 6164 addpiord 7148 mulpiord 7149 addvalex 7676 cnref1o 9469 ioof 9784 frecuzrdgrrn 10212 frec2uzrdg 10213 frecuzrdgrcl 10214 frecuzrdgsuc 10218 frecuzrdgrclt 10219 frecuzrdgg 10220 frecuzrdgsuctlem 10227 seq3val 10262 seqvalcd 10263 cnrecnv 10714 eucalgval 11771 eucalginv 11773 eucalglt 11774 eucalg 11776 sqpweven 11889 2sqpwodd 11890 isstructim 12012 isstructr 12013 txdis1cn 12486 lmcn2 12488 cnmpt12f 12494 cnmpt21 12499 cnmpt2t 12501 cnmpt22 12502 psmetxrge0 12540 xmeterval 12643 comet 12707 txmetcnp 12726 qtopbasss 12729 cnmetdval 12737 remetdval 12747 tgqioo 12755 |
Copyright terms: Public domain | W3C validator |