Definition df-aov 47899

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

This definition is used by:  aoveq123d  47956  nfaov  47957  aovfundmoveq  47959  aovnfundmuv  47960  ndmaov  47961  aovvdm  47963  nfunsnaov  47964  aovvfunressn  47965  aovprc  47966  aovrcl  47967  aovpcov0  47968  aovnuoveq  47969  aovvoveq  47970  aov0ov0  47971  aovovn0oveq  47972  aov0nbovbi  47973  aovov0bi  47974  fnotaovb  47976  ffnaov  47977  aoprssdm  47980