Theorem nff

Description: Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nff.1	|- F/_ x F
	nff.2	|- F/_ x A
	nff.3	|- F/_ x B
Assertion	nff	|- F/ x F : A --> B

Proof

Step	Hyp	Ref	Expression
1		nff.1	|- F/_ x F
2		nff.2	|- F/_ x A
3		nff.3	|- F/_ x B
4		df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	1 2	nffn	|- F/ x F Fn A
6	1	nfrn	|- F/_ x ran F
7	6 3	nfss	|- F/ x ran F C_ B
8	5 7	nfan	|- F/ x ( F Fn A /\ ran F C_ B )
9	4 8	nfxfr	|- F/ x F : A --> B