# Metamath Proof Explorer

## Theorem nfnf

Description: If x is not free in ph , it is not free in F/ y ph . (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017)

Ref Expression
Hypothesis nfnf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion nfnf ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 nfnf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 df-nf ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 1 nfex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 1 nfal ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 3 4 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 2 5 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$