Description: Version of bj-ceqsalt with a disjoint variable condition on
x , V , removing dependency on df-sb and df-clab . Prefer its
use over bj-ceqsalt when sufficient (in particular when V is
substituted for _V ). (Contributed by BJ, 16-Jun-2019)(Proof modification is discouraged.)