Definition df-aov 38619

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

This definition is referenced by:  aoveq123d  38680  nfaov  38681  aovfundmoveq  38683  aovnfundmuv  38684  ndmaov  38685  aovvdm  38687  nfunsnaov  38688  aovvfunressn  38689  aovprc  38690  aovrcl  38691  aovpcov0  38692  aovnuoveq  38693  aovvoveq  38694  aov0ov0  38695  aovovn0oveq  38696  aov0nbovbi  38697  aovov0bi  38698  fnotaovb  38700  ffnaov  38701  aoprssdm  38704