Definition df-aov 48397

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

This definition is used by:  aoveq123d  48453  nfaov  48454  aovfundmoveq  48456  aovnfundmuv  48457  ndmaov  48458  aovvdm  48460  nfunsnaov  48461  aovvfunressn  48462  aovprc  48463  aovrcl  48464  aovpcov0  48465  aovnuoveq  48466  aovvoveq  48467  aov0ov0  48468  aovovn0oveq  48469  aov0nbovbi  48470  aovov0bi  48471  fnotaovb  48473  ffnaov  48474  aoprssdm  48477