Description: Version of bj-elisset with a disjoint variable condition on
x , V . This proof uses only df-ex , ax-gen , ax-4 and
df-clel on top of propositional calculus. Prefer its use over
bj-elisset when sufficient. (Contributed by BJ, 14-Sep-2019)(Proof modification is discouraged.)