Theorem fovrn

Description: An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	fovrn	|- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	|- ( ( A e. R /\ B e. S ) -> <. A , B >. e. ( R X. S ) )
2		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
3		ffvelrn	|- ( ( F : ( R X. S ) --> C /\ <. A , B >. e. ( R X. S ) ) -> ( F ` <. A , B >. ) e. C )
4	2 3	eqeltrid	|- ( ( F : ( R X. S ) --> C /\ <. A , B >. e. ( R X. S ) ) -> ( A F B ) e. C )
5	1 4	sylan2	|- ( ( F : ( R X. S ) --> C /\ ( A e. R /\ B e. S ) ) -> ( A F B ) e. C )
6	5	3impb	|- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C )