Definition df-aov 47106

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

This definition is referenced by:  aoveq123d  47163  nfaov  47164  aovfundmoveq  47166  aovnfundmuv  47167  ndmaov  47168  aovvdm  47170  nfunsnaov  47171  aovvfunressn  47172  aovprc  47173  aovrcl  47174  aovpcov0  47175  aovnuoveq  47176  aovvoveq  47177  aov0ov0  47178  aovovn0oveq  47179  aov0nbovbi  47180  aovov0bi  47181  fnotaovb  47183  ffnaov  47184  aoprssdm  47187