Theorem ffnfvf

Description: A function maps to a class to which all values belong. This version of ffnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Hypotheses	ffnfvf.1	|- F/_ x A
	ffnfvf.2	|- F/_ x B
	ffnfvf.3	|- F/_ x F
Assertion	ffnfvf	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ffnfvf.1	|- F/_ x A
2		ffnfvf.2	|- F/_ x B
3		ffnfvf.3	|- F/_ x F
4		ffnfv	|- ( F : A --> B <-> ( F Fn A /\ A. z e. A ( F ` z ) e. B ) )
5		nfcv	|- F/_ z A
6		nfcv	|- F/_ x z
7	3 6	nffv	|- F/_ x ( F ` z )
8	7 2	nfel	|- F/ x ( F ` z ) e. B
9		nfv	|- F/ z ( F ` x ) e. B
10		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
11	10	eleq1d	|- ( z = x -> ( ( F ` z ) e. B <-> ( F ` x ) e. B ) )
12	5 1 8 9 11	cbvralfw	|- ( A. z e. A ( F ` z ) e. B <-> A. x e. A ( F ` x ) e. B )
13	12	anbi2i	|- ( ( F Fn A /\ A. z e. A ( F ` z ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
14	4 13	bitri	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )