Definition df-aov 44146

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

This definition is referenced by:  aoveq123d  44203  nfaov  44204  aovfundmoveq  44206  aovnfundmuv  44207  ndmaov  44208  aovvdm  44210  nfunsnaov  44211  aovvfunressn  44212  aovprc  44213  aovrcl  44214  aovpcov0  44215  aovnuoveq  44216  aovvoveq  44217  aov0ov0  44218  aovovn0oveq  44219  aov0nbovbi  44220  aovov0bi  44221  fnotaovb  44223  ffnaov  44224  aoprssdm  44227