Metamath Proof Explorer


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 (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )