Theorem sbiedv

Conversion of implicit substitution to explicit substitution (deduction version of sbie ). Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker sbiedvw when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.)

Hypothesis
sbiedv.1
\( \vdash \varphi \wedge x = y' \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / x ] \, \psi \leftrightarrow \chi) \)
Proof
l0
nfv
l1
nfvd
sbiedv.1
ex _
sbied l0 l1 _