Definition df-aov 47470

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

This definition is referenced by:  aoveq123d  47527  nfaov  47528  aovfundmoveq  47530  aovnfundmuv  47531  ndmaov  47532  aovvdm  47534  nfunsnaov  47535  aovvfunressn  47536  aovprc  47537  aovrcl  47538  aovpcov0  47539  aovnuoveq  47540  aovvoveq  47541  aov0ov0  47542  aovovn0oveq  47543  aov0nbovbi  47544  aovov0bi  47545  fnotaovb  47547  ffnaov  47548  aoprssdm  47551