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 28079
Description: Define the value of an operation. In contrast to df-ov 5877, the alternative definition for a function value ( see df-afv 28078) 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 28076 . 2  class (( A F B))
51, 2cop 3656 . . 3  class  <. A ,  B >.
65, 3cafv 28075 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1632 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  aoveq123d  28146  nfaov  28147  aovfundmoveq  28149  aovnfundmuv  28150  ndmaov  28151  aovvdm  28153  nfunsnaov  28154  aovvfunressn  28155  aovprc  28156  aovrcl  28157  aovpcov0  28158  aovnuoveq  28159  aovvoveq  28160  aov0ov0  28161  aovovn0oveq  28162  aov0nbovbi  28163  aovov0bi  28164  fnotaovb  28166  ffnaov  28167  aoprssdm  28170
  Copyright terms: Public domain W3C validator