# Metamath Proof Explorer

## Theorem wl-sbnf1

Description: Two ways expressing that x is effectively not free in ph . Simplified version of sbnf2 . Note: This theorem shows that sbnf2 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019)

Ref Expression
Assertion wl-sbnf1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left[{y}/{x}\right]{\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 nf5 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 wl-sbhbt ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left[{y}/{x}\right]{\phi }\right)\right)$
4 2 3 albid ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left[{y}/{x}\right]{\phi }\right)\right)$
5 1 4 syl5bb ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left[{y}/{x}\right]{\phi }\right)\right)$