Definition df-aov 48284

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

This definition is used by:  aoveq123d  48341  nfaov  48342  aovfundmoveq  48344  aovnfundmuv  48345  ndmaov  48346  aovvdm  48348  nfunsnaov  48349  aovvfunressn  48350  aovprc  48351  aovrcl  48352  aovpcov0  48353  aovnuoveq  48354  aovvoveq  48355  aov0ov0  48356  aovovn0oveq  48357  aov0nbovbi  48358  aovov0bi  48359  fnotaovb  48361  ffnaov  48362  aoprssdm  48365