Definition df-aov 47122

Description: Define the value of an operation. In contrast to df-ov 7390, the alternative definition for a function value (see df-afv 47121) 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 47119	. 2 class ((𝐴𝐹𝐵))
5	1, 2	cop 4595	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cafv 47118	. 2 class (𝐹'''⟨𝐴, 𝐵⟩)
7	4, 6	wceq 1540	1 wff ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)

This definition is referenced by:  aoveq123d  47179  nfaov  47180  aovfundmoveq  47182  aovnfundmuv  47183  ndmaov  47184  aovvdm  47186  nfunsnaov  47187  aovvfunressn  47188  aovprc  47189  aovrcl  47190  aovpcov0  47191  aovnuoveq  47192  aovvoveq  47193  aov0ov0  47194  aovovn0oveq  47195  aov0nbovbi  47196  aovov0bi  47197  fnotaovb  47199  ffnaov  47200  aoprssdm  47203