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