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

Definition df-aov 27388
Description: Define the value of an operation. In contrast to df-ov 5861, the alternative definition for a function value ( see df-afv 27387) 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 27385 . 2  class (( A F B))
51, 2cop 3643 . . 3  class  <. A ,  B >.
65, 3cafv 27384 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1623 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  aoveq123d  27450  nfaov  27451  aovfundmoveq  27453  aovnfundmuv  27454  ndmaov  27455  aovvdm  27457  nfunsnaov  27458  aovvfunressn  27459  aovprc  27460  aovrcl  27461  aovpcov0  27462  aovnuoveq  27463  aovvoveq  27464  aov0ov0  27465  aovovn0oveq  27466  aov0nbovbi  27467  aovov0bi  27468  fnotaovb  27470  ffnaov  27471  aoprssdm  27474
  Copyright terms: Public domain W3C validator