Users' Mathboxes 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 43305
Description: Define the value of an operation. In contrast to df-ov 7151, the alternative definition for a function value (see df-afv 43304) 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 43302 . 2 class ((𝐴𝐹𝐵))
51, 2cop 4565 . . 3 class 𝐴, 𝐵
65, 3cafv 43301 . 2 class (𝐹'''⟨𝐴, 𝐵⟩)
74, 6wceq 1530 1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  aoveq123d  43362  nfaov  43363  aovfundmoveq  43365  aovnfundmuv  43366  ndmaov  43367  aovvdm  43369  nfunsnaov  43370  aovvfunressn  43371  aovprc  43372  aovrcl  43373  aovpcov0  43374  aovnuoveq  43375  aovvoveq  43376  aov0ov0  43377  aovovn0oveq  43378  aov0nbovbi  43379  aovov0bi  43380  fnotaovb  43382  ffnaov  43383  aoprssdm  43386
  Copyright terms: Public domain W3C validator