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 38619
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  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 38616 . 2  class (( A F B))
51, 2cop 3974 . . 3  class  <. A ,  B >.
65, 3cafv 38615 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1444 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
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