# Metamath Proof Explorer

## Theorem nfexd

Description: If x is not free in ps , it is not free in E. y ps . (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypotheses nfald.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfald.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfexd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 nfald.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfald.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 df-ex ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
4 2 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
5 1 4 nfald ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
6 5 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 3 6 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$