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 31993
Description: Define the value of an operation. In contrast to df-ov 6298, the alternative definition for a function value (see df-afv 31992) 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 31990 . 2  class (( A F B))
51, 2cop 4039 . . 3  class  <. A ,  B >.
65, 3cafv 31989 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1379 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  aoveq123d  32053  nfaov  32054  aovfundmoveq  32056  aovnfundmuv  32057  ndmaov  32058  aovvdm  32060  nfunsnaov  32061  aovvfunressn  32062  aovprc  32063  aovrcl  32064  aovpcov0  32065  aovnuoveq  32066  aovvoveq  32067  aov0ov0  32068  aovovn0oveq  32069  aov0nbovbi  32070  aovov0bi  32071  fnotaovb  32073  ffnaov  32074  aoprssdm  32077
  Copyright terms: Public domain W3C validator