Definition df-aov 47036

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

This definition is referenced by:  aoveq123d  47093  nfaov  47094  aovfundmoveq  47096  aovnfundmuv  47097  ndmaov  47098  aovvdm  47100  nfunsnaov  47101  aovvfunressn  47102  aovprc  47103  aovrcl  47104  aovpcov0  47105  aovnuoveq  47106  aovvoveq  47107  aov0ov0  47108  aovovn0oveq  47109  aov0nbovbi  47110  aovov0bi  47111  fnotaovb  47113  ffnaov  47114  aoprssdm  47117