Theorem sbhb

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

Conclusion
\( \vdash \varphi \rightarrow \forall x \, \varphi \leftrightarrow \forall y \, (\varphi \rightarrow [ y / x ] \, \varphi) \)
Proof
nfv
sb8 _
l2
imbi2i _
\( \vdash \varphi \rightarrow \forall x \, \varphi \leftrightarrow \varphi \rightarrow \forall y \, [ y / x ] \, \varphi \)
19.21v
\( \vdash \forall y \, (\varphi \rightarrow [ y / x ] \, \varphi) \leftrightarrow \varphi \rightarrow \forall y \, [ y / x ] \, \varphi \)
bitr4i l2 _