Description: Version of aecoms with a disjoint variable condition, provable from
Tarski's FOL. The corresponding version of naecoms should not be very
useful since -. A. x x = y , DV ( x , y ) is true when the
universe has at least two objects (see dtru ). (Contributed by BJ, 31-May-2019)(Proof modification is discouraged.)