Definition df-aov 47071

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

This definition is referenced by:  aoveq123d  47128  nfaov  47129  aovfundmoveq  47131  aovnfundmuv  47132  ndmaov  47133  aovvdm  47135  nfunsnaov  47136  aovvfunressn  47137  aovprc  47138  aovrcl  47139  aovpcov0  47140  aovnuoveq  47141  aovvoveq  47142  aov0ov0  47143  aovovn0oveq  47144  aov0nbovbi  47145  aovov0bi  47146  fnotaovb  47148  ffnaov  47149  aoprssdm  47152