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