Definition df-aov 47569

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

Assertion

Ref	Expression
df-aov	⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-aov

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	caov 47566	. 2 class ((𝐴𝐹𝐵))
5	1, 2	cop 4573	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cafv 47565	. 2 class (𝐹'''⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1542	1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

This definition is referenced by:  aoveq123d  47626  nfaov  47627  aovfundmoveq  47629  aovnfundmuv  47630  ndmaov  47631  aovvdm  47633  nfunsnaov  47634  aovvfunressn  47635  aovprc  47636  aovrcl  47637  aovpcov0  47638  aovnuoveq  47639  aovvoveq  47640  aov0ov0  47641  aovovn0oveq  47642  aov0nbovbi  47643  aovov0bi  47644  fnotaovb  47646  ffnaov  47647  aoprssdm  47650