Definition df-aov 47150

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

This definition is referenced by:  aoveq123d  47207  nfaov  47208  aovfundmoveq  47210  aovnfundmuv  47211  ndmaov  47212  aovvdm  47214  nfunsnaov  47215  aovvfunressn  47216  aovprc  47217  aovrcl  47218  aovpcov0  47219  aovnuoveq  47220  aovvoveq  47221  aov0ov0  47222  aovovn0oveq  47223  aov0nbovbi  47224  aovov0bi  47225  fnotaovb  47227  ffnaov  47228  aoprssdm  47231