Theorem ffnfv

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003)

	Ref	Expression
Assertion	ffnfv	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	|- ( F : A --> B -> F Fn A )
2		ffvelrn	|- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva	|- ( F : A --> B -> A. x e. A ( F ` x ) e. B )
4	1 3	jca	|- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5		simpl	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
6		fvelrnb	|- ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
7	6	biimpd	|- ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
8		nfra1	|- F/ x A. x e. A ( F ` x ) e. B
9		nfv	|- F/ x y e. B
10		rsp	|- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1	|- ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
12	11	biimpcd	|- ( ( F ` x ) e. B -> ( ( F ` x ) = y -> y e. B ) )
13	10 12	syl6	|- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
14	8 9 13	rexlimd	|- ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15	7 14	sylan9	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16	15	ssrdv	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18	5 16 17	sylanbrc	|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> B )
19	4 18	impbii	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )