Description: Variable substitution in unique existential quantifier. Usage of this
theorem is discouraged because it depends on ax-13 . For a version
requiring more disjoint variables, but fewer axioms, see sb8euv .
(Contributed by NM, 7-Aug-1994)(Revised by Mario Carneiro, 7-Oct-2016)(Proof shortened by Wolf Lammen, 24-Aug-2019)(New usage is discouraged.)