Theorem fnovrn

Description: An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007)

	Ref	Expression
Assertion	fnovrn	|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( C F D ) e. ran F )

Proof

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