Definition df-aov 44857

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

This definition is referenced by:  aoveq123d  44914  nfaov  44915  aovfundmoveq  44917  aovnfundmuv  44918  ndmaov  44919  aovvdm  44921  nfunsnaov  44922  aovvfunressn  44923  aovprc  44924  aovrcl  44925  aovpcov0  44926  aovnuoveq  44927  aovvoveq  44928  aov0ov0  44929  aovovn0oveq  44930  aov0nbovbi  44931  aovov0bi  44932  fnotaovb  44934  ffnaov  44935  aoprssdm  44938