Definition df-aov 47581

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

This definition is referenced by:  aoveq123d  47638  nfaov  47639  aovfundmoveq  47641  aovnfundmuv  47642  ndmaov  47643  aovvdm  47645  nfunsnaov  47646  aovvfunressn  47647  aovprc  47648  aovrcl  47649  aovpcov0  47650  aovnuoveq  47651  aovvoveq  47652  aov0ov0  47653  aovovn0oveq  47654  aov0nbovbi  47655  aovov0bi  47656  fnotaovb  47658  ffnaov  47659  aoprssdm  47662