# Metamath Proof Explorer

## Theorem nfsbv

Description: If z is not free in ph , it is not free in [ y / x ] ph when z is distinct from x and y . Version of nfsb requiring more disjoint variables, but fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016) (Revised by Wolf Lammen, 7-Feb-2023) Remove disjoint variable condition on x , y . (Revised by Steven Nguyen, 13-Aug-2023)

Ref Expression
Hypothesis nfsbv.nf ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion nfsbv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 nfsbv.nf ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
2 df-sb ${⊢}\left[{y}/{x}\right]{\phi }↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)$
3 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}={y}$
4 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{x}={w}$
5 4 1 nfim ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)$
6 5 nfal ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)$
7 3 6 nfim ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)$
8 7 nfal ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)$
9 2 8 nfxfr ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$