Theorem sbft

Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \varphi) \)
Proof
l0
spsbe
\( \vdash [ y' / x ] \, \varphi \rightarrow \exists x \, \varphi \)
19.9t
\( \vdash \Finv x \, \varphi \rightarrow (\exists x \, \varphi \leftrightarrow \varphi) \)
l2
imbitrid l0 _
l3
nf5r
\( \vdash \Finv x \, \varphi \rightarrow \varphi \rightarrow \forall x \, \varphi \)
stdpc4
\( \vdash \forall x \, \varphi \rightarrow [ y' / x ] \, \varphi \)
syl6 l3 _
impbid l2 _