Description: Version of bj-isseti 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-isseti when sufficient
(in particular when V is substituted for _V ). (Contributed by BJ, 14-Sep-2019)(Proof modification is discouraged.)