Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-aov | Structured version Visualization version GIF version |
Description: Define the value of an operation. In contrast to df-ov 6653, the alternative definition for a function value (see df-afv 41197) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still 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. (Contributed by Alexander van der Vekens, 26-May-2017.) |
Ref | Expression |
---|---|
df-aov | ⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | caov 41195 | . 2 class ((𝐴𝐹𝐵)) |
5 | 1, 2 | cop 4183 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cafv 41194 | . 2 class (𝐹'''〈𝐴, 𝐵〉) |
7 | 4, 6 | wceq 1483 | 1 wff ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) |
Colors of variables: wff setvar class |
This definition is referenced by: aoveq123d 41258 nfaov 41259 aovfundmoveq 41261 aovnfundmuv 41262 ndmaov 41263 aovvdm 41265 nfunsnaov 41266 aovvfunressn 41267 aovprc 41268 aovrcl 41269 aovpcov0 41270 aovnuoveq 41271 aovvoveq 41272 aov0ov0 41273 aovovn0oveq 41274 aov0nbovbi 41275 aovov0bi 41276 fnotaovb 41278 ffnaov 41279 aoprssdm 41282 |
Copyright terms: Public domain | W3C validator |