Description: Version of rexcom4b and bj-rexcom4b with a disjoint variable
condition on x , V , hence removing dependency on df-sb and
df-clab (so that it depends on df-clel and df-rex only on top of
first-order logic). Prefer its use over bj-rexcom4b when sufficient
(in particular when V is substituted for _V ). Note the V
in the hypothesis instead of _V . (Contributed by BJ, 14-Sep-2019)(Proof modification is discouraged.)