Metamath Proof Explorer


Theorem aovvoveq

Description: The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion aovvoveq A F B C A F B = A F B

Proof

Step Hyp Ref Expression
1 df-aov A F B = F ''' A B
2 1 eleq1i A F B C F ''' A B C
3 afvvfveq F ''' A B C F ''' A B = F A B
4 df-ov A F B = F A B
5 3 1 4 3eqtr4g F ''' A B C A F B = A F B
6 2 5 sylbi A F B C A F B = A F B