# Metamath Proof Explorer

## Theorem nffvd

Description: Deduction version of bound-variable hypothesis builder nffv . (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nffvd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
nffvd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nffvd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 nffvd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 nffvd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfaba1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}$
4 nfaba1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}$
5 3 4 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}\left(\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}\right)$
6 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
7 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
8 6 7 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\right)$
9 abidnf ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}={F}$
10 9 adantr ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}={F}$
11 abidnf ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$
12 11 adantl ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$
13 10 12 fveq12d ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}\left(\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}\right)={F}\left({A}\right)$
14 8 13 nfceqdf ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\right)\to \left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}\left(\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}\right)↔\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)\right)$
15 1 2 14 syl2anc ${⊢}{\phi }\to \left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {F}\right\}\left(\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}\right)↔\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)\right)$
16 5 15 mpbii ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)$