Definition df-aov 44564

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

This definition is referenced by:  aoveq123d  44621  nfaov  44622  aovfundmoveq  44624  aovnfundmuv  44625  ndmaov  44626  aovvdm  44628  nfunsnaov  44629  aovvfunressn  44630  aovprc  44631  aovrcl  44632  aovpcov0  44633  aovnuoveq  44634  aovvoveq  44635  aov0ov0  44636  aovovn0oveq  44637  aov0nbovbi  44638  aovov0bi  44639  fnotaovb  44641  ffnaov  44642  aoprssdm  44645