Theorem nff

Description: Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nff.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nff.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nff.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		df-f	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
5	1 2	nffn	$$⊢ℲxFFnA$$
6	1	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}F$$
7	6 3	nfss	$$⊢Ⅎx\mathrm{ran}F\subseteq B$$
8	5 7	nfan	$$⊢Ⅎx\left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
9	4 8	nfxfr	$$⊢ℲxF:A⟶B$$