Theorem sbievw

Conversion of implicit substitution to explicit substitution. Version of sbie and sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Aug-2025.)

Hypothesis
sbievw.is
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Proof
sbievw.is
l1
sbbiiev _
\( \vdash [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \psi \)
sbv
\( \vdash [ y' / x ] \, \psi \leftrightarrow \psi \)
bitri l1 _