# Metamath Proof Explorer

## Theorem nfafv2

Description: Bound-variable hypothesis builder for function value, analogous to nffv . To prove a deduction version of this analogous to nffvd is not easily possible because a deduction version of nfdfat cannot be shown easily. (Contributed by AV, 4-Sep-2022)

Ref Expression
Hypotheses nfafv2.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
nfafv2.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nfafv2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)$

### Proof

Step Hyp Ref Expression
1 nfafv2.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 nfafv2.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 df-afv2 ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=if\left({F}\mathrm{defAt}{A},\left(\iota {y}|{A}{F}{y}\right),𝒫\bigcup \mathrm{ran}{F}\right)$
4 1 2 nfdfat ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\mathrm{defAt}{A}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
6 2 1 5 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}{F}{y}$
7 6 nfiotaw ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\iota {y}|{A}{F}{y}\right)$
8 1 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}$
9 8 nfuni ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{F}$
10 9 nfpw ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}𝒫\bigcup \mathrm{ran}{F}$
11 4 7 10 nfif ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left({F}\mathrm{defAt}{A},\left(\iota {y}|{A}{F}{y}\right),𝒫\bigcup \mathrm{ran}{F}\right)$
12 3 11 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)$