Theorem sbie

Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev and sbievw. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)

Hypotheses
sbie.1
\( \vdash \Finv x \, \psi \)
sbie.2
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Proof
l0
equsb1
\( \vdash [ y' / x ] \, x = y' \)
sbie.2
sbimi _
\( \vdash [ y' / x ] \, x = y' \rightarrow [ y' / x ] \, (\varphi \leftrightarrow \psi) \)
l3
ax-mp l0 _
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \psi) \)
sbie.1
sbf _
sblbis _
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \psi) \leftrightarrow ([ y' / x ] \, \varphi \leftrightarrow \psi) \)
mpbi l3 _