Definition df-aov 43677

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

This definition is referenced by:  aoveq123d  43734  nfaov  43735  aovfundmoveq  43737  aovnfundmuv  43738  ndmaov  43739  aovvdm  43741  nfunsnaov  43742  aovvfunressn  43743  aovprc  43744  aovrcl  43745  aovpcov0  43746  aovnuoveq  43747  aovvoveq  43748  aov0ov0  43749  aovovn0oveq  43750  aov0nbovbi  43751  aovov0bi  43752  fnotaovb  43754  ffnaov  43755  aoprssdm  43758