Theorem
sbf2
Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
Conclusion
\( \vdash [ y' / x ] \, \forall x \, \varphi \leftrightarrow \forall x \, \varphi \)
Proof
nfa1
sbf
_
This is the content in the right pane.