Theorem ovres

Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006)

	Ref	Expression
Assertion	ovres	|- ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
2	1	fvresd	|- ( ( A e. C /\ B e. D ) -> ( ( F |` ( C X. D ) ) ` <. A , B >. ) = ( F ` <. A , B >. ) )
3		df-ov	|- ( A ( F |` ( C X. D ) ) B ) = ( ( F |` ( C X. D ) ) ` <. A , B >. )
4		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
5	2 3 4	3eqtr4g	|- ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )