Description: 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)