Definition df-aov 47133

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

This definition is referenced by:  aoveq123d  47190  nfaov  47191  aovfundmoveq  47193  aovnfundmuv  47194  ndmaov  47195  aovvdm  47197  nfunsnaov  47198  aovvfunressn  47199  aovprc  47200  aovrcl  47201  aovpcov0  47202  aovnuoveq  47203  aovvoveq  47204  aov0ov0  47205  aovovn0oveq  47206  aov0nbovbi  47207  aovov0bi  47208  fnotaovb  47210  ffnaov  47211  aoprssdm  47214