Theorem bj-elissetv

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.)

	Ref	Expression
Assertion	bj-elissetv	$$⊢A\in V\to \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢A\in V\leftrightarrow \exists x\left(x=A\wedge x\in V\right)$$
2		exsimpl	$$⊢\exists x\left(x=A\wedge x\in V\right)\to \exists xx=A$$
3	1 2	sylbi	$$⊢A\in V\to \exists xx=A$$