Description: Substitution of variable in existential quantifier. Usage of this
theorem is discouraged because it depends on ax-13 . For a version
requiring disjoint variables, but fewer axioms, see sb8ev .
(Contributed by NM, 12-Aug-1993)(Revised by Mario Carneiro, 6-Oct-2016)(Proof shortened by Jim Kingdon, 15-Jan-2018)(New usage is discouraged.)