Definition df-aov 38034

Description: Define the value of an operation. In contrast to df-ov 6308, the alternative definition for a function value (see df-afv 38033) 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 F and its arguments A and B- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)

Assertion

Ref	Expression
df-aov	|- (( A F B)) = ( F''' <. A , B >. )

Detailed syntax breakdown of Definition df-aov

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	caov 38031	. 2 class (( A F B))
5	1, 2	cop 4008	. . 3 class <. A , B >.
6	5, 3	cafv 38030	. 2 class ( F''' <. A , B >. )
7	4, 6	wceq 1437	1 wff (( A F B)) = ( F''' <. A , B >. )

This definition is referenced by:  aoveq123d  38094  nfaov  38095  aovfundmoveq  38097  aovnfundmuv  38098  ndmaov  38099  aovvdm  38101  nfunsnaov  38102  aovvfunressn  38103  aovprc  38104  aovrcl  38105  aovpcov0  38106  aovnuoveq  38107  aovvoveq  38108  aov0ov0  38109  aovovn0oveq  38110  aov0nbovbi  38111  aovov0bi  38112  fnotaovb  38114  ffnaov  38115  aoprssdm  38118