Theorem nff1o

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

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

Proof

Step	Hyp	Ref	Expression
1		nff1o.1	|- F/_ x F
2		nff1o.2	|- F/_ x A
3		nff1o.3	|- F/_ x B
4		df-f1o	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
5	1 2 3	nff1	|- F/ x F : A -1-1-> B
6	1 2 3	nffo	|- F/ x F : A -onto-> B
7	5 6	nfan	|- F/ x ( F : A -1-1-> B /\ F : A -onto-> B )
8	4 7	nfxfr	|- F/ x F : A -1-1-onto-> B