Theorem sbiedw

Conversion of implicit substitution to explicit substitution (deduction version of sbiev ). Version of sbied with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypotheses
sbiedw.1
\( \vdash \Finv x \, \varphi \)
sbiedw.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
sbiedw.3
\( \vdash \varphi \rightarrow x = y' \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / x ] \, \psi \leftrightarrow \chi) \)
Proof
sbiedw.1
l1
sbrim _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
l2
sbiedw.1
sbiedw.2
l4
nfim1 l2 _
sbiedw.3
com12 _
pm5.74d _
sbiev l4 _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \chi \)
bitr3i l1 _
pm5.74ri _