Definition df-aov 47226

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

This definition is referenced by:  aoveq123d  47283  nfaov  47284  aovfundmoveq  47286  aovnfundmuv  47287  ndmaov  47288  aovvdm  47290  nfunsnaov  47291  aovvfunressn  47292  aovprc  47293  aovrcl  47294  aovpcov0  47295  aovnuoveq  47296  aovvoveq  47297  aov0ov0  47298  aovovn0oveq  47299  aov0nbovbi  47300  aovov0bi  47301  fnotaovb  47303  ffnaov  47304  aoprssdm  47307