Definition df-aov 48017

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

This definition is used by:  aoveq123d  48074  nfaov  48075  aovfundmoveq  48077  aovnfundmuv  48078  ndmaov  48079  aovvdm  48081  nfunsnaov  48082  aovvfunressn  48083  aovprc  48084  aovrcl  48085  aovpcov0  48086  aovnuoveq  48087  aovvoveq  48088  aov0ov0  48089  aovovn0oveq  48090  aov0nbovbi  48091  aovov0bi  48092  fnotaovb  48094  ffnaov  48095  aoprssdm  48098