# Metamath Proof Explorer

## Theorem nffun

Description: Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004)

Ref Expression
Hypothesis nffun.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
Assertion nffun ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{F}$

### Proof

Step Hyp Ref Expression
1 nffun.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 df-fun ${⊢}\mathrm{Fun}{F}↔\left(\mathrm{Rel}{F}\wedge {F}\circ {{F}}^{-1}\subseteq \mathrm{I}\right)$
3 1 nfrel ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{F}$
4 1 nfcnv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}$
5 1 4 nfco ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({F}\circ {{F}}^{-1}\right)$
6 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{I}$
7 5 6 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\circ {{F}}^{-1}\subseteq \mathrm{I}$
8 3 7 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Rel}{F}\wedge {F}\circ {{F}}^{-1}\subseteq \mathrm{I}\right)$
9 2 8 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{F}$