Theorem sb4av

Version of sb4a with a disjoint variable condition, which does not require [ax-13]. The distinctor antecedent from sb4b is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.)

Conclusion
\( \vdash [ t / x ] \, \forall t \, \varphi \rightarrow \forall x \, (x = t \rightarrow \varphi) \)
Proof
sp
l1
sbimi _
\( \vdash [ t / x ] \, \forall t \, \varphi \rightarrow [ t / x ] \, \varphi \)
sb6
\( \vdash [ t / x ] \, \varphi \leftrightarrow \forall x \, (x = t \rightarrow \varphi) \)
sylib l1 _