Definition df-aov 41198

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

This definition is referenced by:  aoveq123d  41258  nfaov  41259  aovfundmoveq  41261  aovnfundmuv  41262  ndmaov  41263  aovvdm  41265  nfunsnaov  41266  aovvfunressn  41267  aovprc  41268  aovrcl  41269  aovpcov0  41270  aovnuoveq  41271  aovvoveq  41272  aov0ov0  41273  aovovn0oveq  41274  aov0nbovbi  41275  aovov0bi  41276  fnotaovb  41278  ffnaov  41279  aoprssdm  41282