Definition df-aov 31993

Description: Define the value of an operation. In contrast to df-ov 6298, the alternative definition for a function value (see df-afv 31992) 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 31990	. 2 class (( A F B))
5	1, 2	cop 4039	. . 3 class <. A , B >.
6	5, 3	cafv 31989	. 2 class ( F''' <. A , B >. )
7	4, 6	wceq 1379	1 wff (( A F B)) = ( F''' <. A , B >. )

This definition is referenced by:  aoveq123d  32053  nfaov  32054  aovfundmoveq  32056  aovnfundmuv  32057  ndmaov  32058  aovvdm  32060  nfunsnaov  32061  aovvfunressn  32062  aovprc  32063  aovrcl  32064  aovpcov0  32065  aovnuoveq  32066  aovvoveq  32067  aov0ov0  32068  aovovn0oveq  32069  aov0nbovbi  32070  aovov0bi  32071  fnotaovb  32073  ffnaov  32074  aoprssdm  32077