Definition df-aov 38764

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

This definition is referenced by:  aoveq123d  38825  nfaov  38826  aovfundmoveq  38828  aovnfundmuv  38829  ndmaov  38830  aovvdm  38832  nfunsnaov  38833  aovvfunressn  38834  aovprc  38835  aovrcl  38836  aovpcov0  38837  aovnuoveq  38838  aovvoveq  38839  aov0ov0  38840  aovovn0oveq  38841  aov0nbovbi  38842  aovov0bi  38843  fnotaovb  38845  ffnaov  38846  aoprssdm  38849