![]() |
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 7396, the alternative definition for a function value (see df-afv 45600) 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 45598 | . 2 class ((𝐴𝐹𝐵)) |
5 | 1, 2 | cop 4628 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cafv 45597 | . 2 class (𝐹'''〈𝐴, 𝐵〉) |
7 | 4, 6 | wceq 1541 | 1 wff ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) |
Colors of variables: wff setvar class |
This definition is referenced by: aoveq123d 45658 nfaov 45659 aovfundmoveq 45661 aovnfundmuv 45662 ndmaov 45663 aovvdm 45665 nfunsnaov 45666 aovvfunressn 45667 aovprc 45668 aovrcl 45669 aovpcov0 45670 aovnuoveq 45671 aovvoveq 45672 aov0ov0 45673 aovovn0oveq 45674 aov0nbovbi 45675 aovov0bi 45676 fnotaovb 45678 ffnaov 45679 aoprssdm 45682 |
Copyright terms: Public domain | W3C validator |