Definition df-aov 47126

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

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