Definition df-aov 45819

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

This definition is referenced by:  aoveq123d  45876  nfaov  45877  aovfundmoveq  45879  aovnfundmuv  45880  ndmaov  45881  aovvdm  45883  nfunsnaov  45884  aovvfunressn  45885  aovprc  45886  aovrcl  45887  aovpcov0  45888  aovnuoveq  45889  aovvoveq  45890  aov0ov0  45891  aovovn0oveq  45892  aov0nbovbi  45893  aovov0bi  45894  fnotaovb  45896  ffnaov  45897  aoprssdm  45900