Metamath Proof Explorer

Theorem oveq

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995)

Ref Expression
Assertion oveq 
|- ( F = G -> ( A F B ) = ( A G B ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( F = G -> ( F ` <. A , B >. ) = ( G ` <. A , B >. ) )
2 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
3 df-ov 
 |-  ( A G B ) = ( G ` <. A , B >. )
4 1 2 3 3eqtr4g 
 |-  ( F = G -> ( A F B ) = ( A G B ) )