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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-aov | ||
2 | 1 | eleq1i | |
3 | afvvfveq | ||
4 | df-ov | ||
5 | 3 1 4 | 3eqtr4g | |
6 | 2 5 | sylbi |