Theorem nff1

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

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

Proof

Step	Hyp	Ref	Expression
1		nff1.1	|- F/_ x F
2		nff1.2	|- F/_ x A
3		nff1.3	|- F/_ x B
4		df-f1	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
5	1 2 3	nff	|- F/ x F : A --> B
6	1	nfcnv	|- F/_ x `' F
7	6	nffun	|- F/ x Fun `' F
8	5 7	nfan	|- F/ x ( F : A --> B /\ Fun `' F )
9	4 8	nfxfr	|- F/ x F : A -1-1-> B