Theorem oveq1

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

	Ref	Expression
Assertion	oveq1	|- ( A = B -> ( A F C ) = ( B F C ) )

Proof

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