Version of 19.9 with a disjoint variable condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v. (Contributed by NM, 28-May-1995.) Remove dependency on [ax-7]. (Revised by Wolf Lammen, 4-Dec-2017.)