# Metamath Proof Explorer

## Theorem sbhb

Description: Two ways of expressing " x is (effectively) not free in ph ". Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-May-2009) (New usage is discouraged.)

Ref Expression
Assertion sbhb ${⊢}\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)$

### Proof

Step Hyp Ref Expression
1 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 sb8 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
3 2 imbi2i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }\right)$
4 19.21v ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left[{y}/{x}\right]{\phi }\right)↔\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }\right)$
5 3 4 bitr4i ${⊢}\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)$