Definition df-aov 47713

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

This definition is referenced by:  aoveq123d  47770  nfaov  47771  aovfundmoveq  47773  aovnfundmuv  47774  ndmaov  47775  aovvdm  47777  nfunsnaov  47778  aovvfunressn  47779  aovprc  47780  aovrcl  47781  aovpcov0  47782  aovnuoveq  47783  aovvoveq  47784  aov0ov0  47785  aovovn0oveq  47786  aov0nbovbi  47787  aovov0bi  47788  fnotaovb  47790  ffnaov  47791  aoprssdm  47794