![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-aov | Structured version Visualization version Unicode version |
Description: Define the value of an
operation. In contrast to df-ov 6293, the
alternative definition for a function value (see df-afv 38618) 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
![]() ![]() ![]() |
Ref | Expression |
---|---|
df-aov |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | caov 38616 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3974 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | cafv 38615 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1444 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: aoveq123d 38680 nfaov 38681 aovfundmoveq 38683 aovnfundmuv 38684 ndmaov 38685 aovvdm 38687 nfunsnaov 38688 aovvfunressn 38689 aovprc 38690 aovrcl 38691 aovpcov0 38692 aovnuoveq 38693 aovvoveq 38694 aov0ov0 38695 aovovn0oveq 38696 aov0nbovbi 38697 aovov0bi 38698 fnotaovb 38700 ffnaov 38701 aoprssdm 38704 |
Copyright terms: Public domain | W3C validator |