Definition df-aov 47591

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

This definition is referenced by:  aoveq123d  47648  nfaov  47649  aovfundmoveq  47651  aovnfundmuv  47652  ndmaov  47653  aovvdm  47655  nfunsnaov  47656  aovvfunressn  47657  aovprc  47658  aovrcl  47659  aovpcov0  47660  aovnuoveq  47661  aovvoveq  47662  aov0ov0  47663  aovovn0oveq  47664  aov0nbovbi  47665  aovov0bi  47666  fnotaovb  47668  ffnaov  47669  aoprssdm  47672