Definition df-aov 47131

Description: Define the value of an operation. In contrast to df-ov 7344, the alternative definition for a function value (see df-afv 47130) 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	caov 47128	. 2 class ((𝐴𝐹𝐵))
5	1, 2	cop 4580	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cafv 47127	. 2 class (𝐹'''⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1541	1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

This definition is referenced by:  aoveq123d  47188  nfaov  47189  aovfundmoveq  47191  aovnfundmuv  47192  ndmaov  47193  aovvdm  47195  nfunsnaov  47196  aovvfunressn  47197  aovprc  47198  aovrcl  47199  aovpcov0  47200  aovnuoveq  47201  aovvoveq  47202  aov0ov0  47203  aovovn0oveq  47204  aov0nbovbi  47205  aovov0bi  47206  fnotaovb  47208  ffnaov  47209  aoprssdm  47212