![]() |
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 6311, the
alternative definition for a function value (see df-afv 38763) 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 38761 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3965 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | cafv 38760 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1452 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: aoveq123d 38825 nfaov 38826 aovfundmoveq 38828 aovnfundmuv 38829 ndmaov 38830 aovvdm 38832 nfunsnaov 38833 aovvfunressn 38834 aovprc 38835 aovrcl 38836 aovpcov0 38837 aovnuoveq 38838 aovvoveq 38839 aov0ov0 38840 aovovn0oveq 38841 aov0nbovbi 38842 aovov0bi 38843 fnotaovb 38845 ffnaov 38846 aoprssdm 38849 |
Copyright terms: Public domain | W3C validator |