![]() |
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 5701 and ovprc2 5702. 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 5672. (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 5668 | . 2 class (𝐴𝐹𝐵) |
5 | 1, 2 | cop 3455 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cfv 5030 | . 2 class (𝐹‘〈𝐴, 𝐵〉) |
7 | 4, 6 | wceq 1290 | 1 wff (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
Colors of variables: wff set class |
This definition is referenced by: oveq 5674 oveq1 5675 oveq2 5676 nfovd 5694 fnovex 5698 ovexg 5699 ovprc 5700 fnotovb 5708 ffnov 5765 eqfnov 5767 fnovim 5769 ovid 5777 ovidig 5778 ov 5780 ovigg 5781 ov6g 5798 ovg 5799 ovres 5800 fovrn 5803 fnrnov 5806 foov 5807 fnovrn 5808 funimassov 5810 ovelimab 5811 ovconst2 5812 elmpt2cl 5858 mpt2fvex 5989 oprab2co 5999 algrflem 6010 algrflemg 6011 mpt2xopn0yelv 6020 ovtposg 6040 addpiord 6938 mulpiord 6939 addvalex 7444 cnref1o 9196 ioof 9452 frecuzrdgrrn 9878 frec2uzrdg 9879 frecuzrdgrcl 9880 frecuzrdgsuc 9884 frecuzrdgrclt 9885 frecuzrdgg 9886 frecuzrdgsuctlem 9893 iseqvalt 9936 seq3val 9937 cnrecnv 10407 eucalgval 11377 eucalginv 11379 eucalglt 11380 eucalg 11382 sqpweven 11494 2sqpwodd 11495 isstructim 11571 isstructr 11572 |
Copyright terms: Public domain | W3C validator |