Definition df-aov 48135

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

This definition is used by:  aoveq123d  48192  nfaov  48193  aovfundmoveq  48195  aovnfundmuv  48196  ndmaov  48197  aovvdm  48199  nfunsnaov  48200  aovvfunressn  48201  aovprc  48202  aovrcl  48203  aovpcov0  48204  aovnuoveq  48205  aovvoveq  48206  aov0ov0  48207  aovovn0oveq  48208  aov0nbovbi  48209  aovov0bi  48210  fnotaovb  48212  ffnaov  48213  aoprssdm  48216