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 40967
Description: Define the value of an operation. In contrast to df-ov 6650, the alternative definition for a function value (see df-afv 40966) 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 40964 . 2 class ((𝐴𝐹𝐵))
51, 2cop 4181 . . 3 class 𝐴, 𝐵
65, 3cafv 40963 . 2 class (𝐹'''⟨𝐴, 𝐵⟩)
74, 6wceq 1482 1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  aoveq123d  41027  nfaov  41028  aovfundmoveq  41030  aovnfundmuv  41031  ndmaov  41032  aovvdm  41034  nfunsnaov  41035  aovvfunressn  41036  aovprc  41037  aovrcl  41038  aovpcov0  41039  aovnuoveq  41040  aovvoveq  41041  aov0ov0  41042  aovovn0oveq  41043  aov0nbovbi  41044  aovov0bi  41045  fnotaovb  41047  ffnaov  41048  aoprssdm  41051
  Copyright terms: Public domain W3C validator