Users' Mathboxes 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

Definition df-aov 38764
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  F and its arguments  A and  B- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)
Assertion
Ref Expression
df-aov  |- (( A F B))  =  ( F''' <. A ,  B >. )

Detailed syntax breakdown of Definition df-aov
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3caov 38761 . 2  class (( A F B))
51, 2cop 3965 . . 3  class  <. A ,  B >.
65, 3cafv 38760 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1452 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
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