Description: Place a conjunct in the scope of an existential quantifier.
(Contributed by NM, 18-Aug-1993)(Proof shortened by Andrew Salmon, 25-May-2011)(Proof shortened by Wolf Lammen, 13-Jan-2018) Reduce
axiom dependencies. (Revised by BJ, 7-Jul-2021)(Proof shortened by Wolf Lammen, 6-Nov-2022) Expand hypothesis. (Revised by Steven
Nguyen, 19-Jun-2023)