Definition df-aov 47235

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

This definition is referenced by:  aoveq123d  47292  nfaov  47293  aovfundmoveq  47295  aovnfundmuv  47296  ndmaov  47297  aovvdm  47299  nfunsnaov  47300  aovvfunressn  47301  aovprc  47302  aovrcl  47303  aovpcov0  47304  aovnuoveq  47305  aovvoveq  47306  aov0ov0  47307  aovovn0oveq  47308  aov0nbovbi  47309  aovov0bi  47310  fnotaovb  47312  ffnaov  47313  aoprssdm  47316