Definition df-aov 39847

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

This definition is referenced by:  aoveq123d  39907  nfaov  39908  aovfundmoveq  39910  aovnfundmuv  39911  ndmaov  39912  aovvdm  39914  nfunsnaov  39915  aovvfunressn  39916  aovprc  39917  aovrcl  39918  aovpcov0  39919  aovnuoveq  39920  aovvoveq  39921  aov0ov0  39922  aovovn0oveq  39923  aov0nbovbi  39924  aovov0bi  39925  fnotaovb  39927  ffnaov  39928  aoprssdm  39931