Version of 19.3 with a disjoint variable condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on [ax-7]. (Revised by Wolf Lammen, 4-Dec-2017.) (Proof shortened by Wolf Lammen, 20-Oct-2023.)