Theorem nffo

Description: Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004)

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

Proof

Step	Hyp	Ref	Expression
1		nffo.1	|- F/_ x F
2		nffo.2	|- F/_ x A
3		nffo.3	|- F/_ x B
4		df-fo	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
5	1 2	nffn	|- F/ x F Fn A
6	1	nfrn	|- F/_ x ran F
7	6 3	nfeq	|- F/ x ran F = B
8	5 7	nfan	|- F/ x ( F Fn A /\ ran F = B )
9	4 8	nfxfr	|- F/ x F : A -onto-> B