Description: Conversion of implicit substitution to explicit substitution (deduction
version of sbie ) Usage of this theorem is discouraged because it
depends on ax-13 . See sbiedw , sbiedvw for variants using
disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994)(Revised by Mario Carneiro, 4-Oct-2016)(Proof
shortened by Wolf Lammen, 24-Jun-2018)(New usage is discouraged.)