Description: Convert implication to equivalence within an existence statement using
the Separation Scheme (Aussonderung) ax-sep . Inference associated
with sepex . (Contributed by NM, 21-Jun-1993) Generalize
conclusion, extract closed form, and avoid ax-9 . (Revised by Matthew
House, 19-Sep-2025)