Definition df-aov 47835

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

This definition is referenced by:  aoveq123d  47892  nfaov  47893  aovfundmoveq  47895  aovnfundmuv  47896  ndmaov  47897  aovvdm  47899  nfunsnaov  47900  aovvfunressn  47901  aovprc  47902  aovrcl  47903  aovpcov0  47904  aovnuoveq  47905  aovvoveq  47906  aov0ov0  47907  aovovn0oveq  47908  aov0nbovbi  47909  aovov0bi  47910  fnotaovb  47912  ffnaov  47913  aoprssdm  47916