Definition df-aov 47679

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

This definition is referenced by:  aoveq123d  47736  nfaov  47737  aovfundmoveq  47739  aovnfundmuv  47740  ndmaov  47741  aovvdm  47743  nfunsnaov  47744  aovvfunressn  47745  aovprc  47746  aovrcl  47747  aovpcov0  47748  aovnuoveq  47749  aovvoveq  47750  aov0ov0  47751  aovovn0oveq  47752  aov0nbovbi  47753  aovov0bi  47754  fnotaovb  47756  ffnaov  47757  aoprssdm  47760