Definition df-aov 45601

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

This definition is referenced by:  aoveq123d  45658  nfaov  45659  aovfundmoveq  45661  aovnfundmuv  45662  ndmaov  45663  aovvdm  45665  nfunsnaov  45666  aovvfunressn  45667  aovprc  45668  aovrcl  45669  aovpcov0  45670  aovnuoveq  45671  aovvoveq  45672  aov0ov0  45673  aovovn0oveq  45674  aov0nbovbi  45675  aovov0bi  45676  fnotaovb  45678  ffnaov  45679  aoprssdm  45682