Definition df-aov 43327

Description: Define the value of an operation. In contrast to df-ov 7161, the alternative definition for a function value (see df-afv 43326) 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 43324	. 2 class ((𝐴𝐹𝐵))
5	1, 2	cop 4575	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cafv 43323	. 2 class (𝐹'''⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1537	1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

This definition is referenced by:  aoveq123d  43384  nfaov  43385  aovfundmoveq  43387  aovnfundmuv  43388  ndmaov  43389  aovvdm  43391  nfunsnaov  43392  aovvfunressn  43393  aovprc  43394  aovrcl  43395  aovpcov0  43396  aovnuoveq  43397  aovvoveq  43398  aov0ov0  43399  aovovn0oveq  43400  aov0nbovbi  43401  aovov0bi  43402  fnotaovb  43404  ffnaov  43405  aoprssdm  43408