Theorem sbiev

Conversion of implicit substitution to explicit substitution. Version of sbie with a disjoint variable condition, not requiring [ax-13]. See sbievw for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on [ax-10] and shorten proof. (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.)

Hypotheses
sbiev.1
\( \vdash \Finv x \, \psi \)
sbiev.2
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Proof
sbiev.2
l1
sbbiiev _
\( \vdash [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \psi \)
sbiev.1
sbf _
\( \vdash [ y' / x ] \, \psi \leftrightarrow \psi \)
bitri l1 _