Theorem nff1

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

	Ref	Expression
Hypotheses	nff1.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nff1.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nff1.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nff1	$$⊢ℲxF:A\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		nff1.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nff1.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nff1.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		df-f1	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$
5	1 2 3	nff	$$⊢ℲxF:A⟶B$$
6	1	nfcnv	$$⊢\underset{\_}{Ⅎ}x{F}^{-1}$$
7	6	nffun	$$⊢Ⅎx\mathrm{Fun}{F}^{-1}$$
8	5 7	nfan	$$⊢Ⅎx\left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$
9	4 8	nfxfr	$$⊢ℲxF:A\underset{1-1}{⟶}B$$