# Metamath Proof Explorer

## Theorem nfovd

Description: Deduction version of bound-variable hypothesis builder nfov . (Contributed by NM, 13-Dec-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

### Proof

Step Hyp Ref Expression
1 nfovd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfovd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
3 nfovd.4 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
4 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
5 1 3 nfopd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩$
6 2 5 nffvd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left(⟨{A},{B}⟩\right)$
7 4 6 nfcxfrd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}{F}{B}\right)$