Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-aov Structured version   Visualization version   GIF version

Definition df-aov 41621
 Description: Define the value of an operation. In contrast to df-ov 6768, the alternative definition for a function value (see df-afv 41620) 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 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)
Assertion
Ref Expression
df-aov ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-aov
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3caov 41618 . 2 class ((𝐴𝐹𝐵))
51, 2cop 4291 . . 3 class 𝐴, 𝐵
65, 3cafv 41617 . 2 class (𝐹'''⟨𝐴, 𝐵⟩)
74, 6wceq 1596 1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
 Colors of variables: wff setvar class This definition is referenced by:  aoveq123d  41681  nfaov  41682  aovfundmoveq  41684  aovnfundmuv  41685  ndmaov  41686  aovvdm  41688  nfunsnaov  41689  aovvfunressn  41690  aovprc  41691  aovrcl  41692  aovpcov0  41693  aovnuoveq  41694  aovvoveq  41695  aov0ov0  41696  aovovn0oveq  41697  aov0nbovbi  41698  aovov0bi  41699  fnotaovb  41701  ffnaov  41702  aoprssdm  41705
 Copyright terms: Public domain W3C validator