Theorem sbv

Substitution for a variable not occurring in a proposition. See sbf for a version without disjoint variable condition on x , ph. If one adds a disjoint variable condition on x , t, then sbv can be proved directly by chaining equsv with sb6. (Contributed by BJ, 22-Dec-2020.)

Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \varphi \)
Proof
l0
spsbe
\( \vdash [ t' / x ] \, \varphi \rightarrow \exists x \, \varphi \)
ax5e
\( \vdash \exists x \, \varphi \rightarrow \varphi \)
l2
syl l0 _
l3
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
stdpc4
\( \vdash \forall x \, \varphi \rightarrow [ t' / x ] \, \varphi \)
syl l3 _
impbii l2 _