Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) Avoid ax-12 . (Revised by Gino Giotto, 12-Oct-2024) (Proof shortened by Wolf Lammen, 22-Jan-2025)