Theorem hbs1

The setvar \( x \) is not free in \( [ y' / x ] \, \varphi \) when \( x \) and \( y' \) are distinct. (Contributed by NM, 26-May-1993.)

Conclusion
\( \vdash [ y' / x ] \, \varphi \rightarrow \forall x \, [ y' / x ] \, \varphi \)
Proof
nfs1v
nf5ri _