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 27943
Description: Define the value of an operation. In contrast to df-ov 6076, the alternative definition for a function value ( see df-afv 27942) 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 27940 . 2  class (( A F B))
51, 2cop 3809 . . 3  class  <. A ,  B >.
65, 3cafv 27939 . 2  class  ( F''' <. A ,  B >. )
74, 6wceq 1652 1  wff (( A F B))  =  ( F''' <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  aoveq123d  28009  nfaov  28010  aovfundmoveq  28012  aovnfundmuv  28013  ndmaov  28014  aovvdm  28016  nfunsnaov  28017  aovvfunressn  28018  aovprc  28019  aovrcl  28020  aovpcov0  28021  aovnuoveq  28022  aovvoveq  28023  aov0ov0  28024  aovovn0oveq  28025  aov0nbovbi  28026  aovov0bi  28027  fnotaovb  28029  ffnaov  28030  aoprssdm  28033
  Copyright terms: Public domain W3C validator