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	$$⊢\underset{\_}{Ⅎ}xF$$
	nff1o.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nff1o.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nff1o	$$⊢ℲxF:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		nff1o.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nff1o.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nff1o.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		df-f1o	$$⊢F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$
5	1 2 3	nff1	$$⊢ℲxF:A\underset{1-1}{⟶}B$$
6	1 2 3	nffo	$$⊢ℲxF:A\underset{onto}{⟶}B$$
7	5 6	nfan	$$⊢Ⅎx\left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$
8	4 7	nfxfr	$$⊢ℲxF:A\underset{1-1\; onto}{⟶}B$$