![]() |
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 A and B- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments A and B 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 A and/or B are proper classes (i.e. are not sets); see ovprc1 5483 and ovprc2 5484. 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 5459. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
df-ov | ⊢ (A𝐹B) = (𝐹‘〈A, B〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | co 5455 | . 2 class (A𝐹B) |
5 | 1, 2 | cop 3370 | . . 3 class 〈A, B〉 |
6 | 5, 3 | cfv 4845 | . 2 class (𝐹‘〈A, B〉) |
7 | 4, 6 | wceq 1242 | 1 wff (A𝐹B) = (𝐹‘〈A, B〉) |
Colors of variables: wff set class |
This definition is referenced by: oveq 5461 oveq1 5462 oveq2 5463 nfovd 5477 fnovex 5481 ovprc 5482 fnotovb 5490 ffnov 5547 eqfnov 5549 fnovim 5551 ovid 5559 ovidig 5560 ov 5562 ovigg 5563 ov6g 5580 ovg 5581 ovres 5582 fovrn 5585 fnrnov 5588 foov 5589 fnovrn 5590 funimassov 5592 ovelimab 5593 ovconst2 5594 elmpt2cl 5640 mpt2fvex 5771 oprab2co 5781 algrflem 5792 mpt2xopn0yelv 5795 ovtposg 5815 addpiord 6300 mulpiord 6301 cnref1o 8357 ioof 8610 frecuzrdgrrn 8875 frec2uzrdg 8876 frecuzrdgsuc 8882 cnrecnv 9138 |
Copyright terms: Public domain | W3C validator |