Definition df-aov 45829

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

This definition is referenced by:  aoveq123d  45886  nfaov  45887  aovfundmoveq  45889  aovnfundmuv  45890  ndmaov  45891  aovvdm  45893  nfunsnaov  45894  aovvfunressn  45895  aovprc  45896  aovrcl  45897  aovpcov0  45898  aovnuoveq  45899  aovvoveq  45900  aov0ov0  45901  aovovn0oveq  45902  aov0nbovbi  45903  aovov0bi  45904  fnotaovb  45906  ffnaov  45907  aoprssdm  45910