Theorem sbf

Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypothesis
sbf.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \varphi \)
Proof
l0
sbf.1
\( \vdash \Finv x \, \varphi \)
sbft
\( \vdash \Finv x \, \varphi \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \varphi) \)
ax-mp l0 _