Definition df-aov 45877

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

This definition is referenced by:  aoveq123d  45934  nfaov  45935  aovfundmoveq  45937  aovnfundmuv  45938  ndmaov  45939  aovvdm  45941  nfunsnaov  45942  aovvfunressn  45943  aovprc  45944  aovrcl  45945  aovpcov0  45946  aovnuoveq  45947  aovvoveq  45948  aov0ov0  45949  aovovn0oveq  45950  aov0nbovbi  45951  aovov0bi  45952  fnotaovb  45954  ffnaov  45955  aoprssdm  45958