# Metamath Proof Explorer

## Theorem bj-sbnf

Description: Move nonfree predicate in and out of substitution; see sbal and sbex . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-sbnf ${⊢}\left[{z}/{y}\right]Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 sbim ${⊢}\left[{z}/{y}\right]\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\left[{z}/{y}\right]{\phi }\to \left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 sbal ${⊢}\left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$
3 2 imbi2i ${⊢}\left(\left[{z}/{y}\right]{\phi }\to \left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\left[{z}/{y}\right]{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\right)$
4 1 3 bitri ${⊢}\left[{z}/{y}\right]\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\left[{z}/{y}\right]{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left[{z}/{y}\right]{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\right)$
6 nf5 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 6 sbbii ${⊢}\left[{z}/{y}\right]Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 sbal ${⊢}\left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 7 8 bitri ${⊢}\left[{z}/{y}\right]Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
10 nf5 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left[{z}/{y}\right]{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\right)$
11 5 9 10 3bitr4i ${⊢}\left[{z}/{y}\right]Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$