Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-aov Structured version   Unicode version

Definition df-aov 38034
Description: Define the value of an operation. In contrast to df-ov 6308, the alternative definition for a function value (see df-afv 38033) 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 38031 . 2  class (( A F B))
51, 2cop 4008 . . 3  class  <. A ,  B >.
65, 3cafv 38030 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1437 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  aoveq123d  38094  nfaov  38095  aovfundmoveq  38097  aovnfundmuv  38098  ndmaov  38099  aovvdm  38101  nfunsnaov  38102  aovvfunressn  38103  aovprc  38104  aovrcl  38105  aovpcov0  38106  aovnuoveq  38107  aovvoveq  38108  aov0ov0  38109  aovovn0oveq  38110  aov0nbovbi  38111  aovov0bi  38112  fnotaovb  38114  ffnaov  38115  aoprssdm  38118
  Copyright terms: Public domain W3C validator