Definition df-aov 47403

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

This definition is referenced by:  aoveq123d  47460  nfaov  47461  aovfundmoveq  47463  aovnfundmuv  47464  ndmaov  47465  aovvdm  47467  nfunsnaov  47468  aovvfunressn  47469  aovprc  47470  aovrcl  47471  aovpcov0  47472  aovnuoveq  47473  aovvoveq  47474  aov0ov0  47475  aovovn0oveq  47476  aov0nbovbi  47477  aovov0bi  47478  fnotaovb  47480  ffnaov  47481  aoprssdm  47484