Theorem sbbiiev

An equivalence of substitutions (as in sbbii) allowing the additional information that \( x = t' \). Version of sbiev and sbievw without a disjoint variable condition on \( \psi \), useful for substituting only part of \( \varphi \). (Contributed by SN, 24-Aug-2025.)

Hypothesis
sbbiiev.1
\( \vdash x = t' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow [ t' / x ] \, \psi \)
Proof
sbbiiev.1
pm5.74i _
l2
albii _
\( \vdash \forall x \, (x = t' \rightarrow \varphi) \leftrightarrow \forall x \, (x = t' \rightarrow \psi) \)
l3
sb6
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall x \, (x = t' \rightarrow \varphi) \)
sb6
\( \vdash [ t' / x ] \, \psi \leftrightarrow \forall x \, (x = t' \rightarrow \psi) \)
3bitr4i l2 l3 _