Definition df-aov

Description: Define the value of an operation. In contrast to df-ov , the alternative definition for a function value (see df-afv ) 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 F and its arguments A and B - will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cF	⊢ 𝐹
2		cB	⊢ 𝐵
3	0 2 1	caov	⊢ (( 𝐴 𝐹 𝐵 ))
4	0 2	cop	⊢ ⟨ 𝐴 , 𝐵 ⟩
5	4 1	cafv	⊢ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
6	3 5	wceq	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )