Theorem elissetv

Description: An element of a class exists. Version of elisset with a disjoint variable condition on V , x , avoiding df-clab . Prefer its use over elisset when sufficient (for instance in usages where x is a dummy variable). (Contributed by BJ, 14-Sep-2019)

	Ref	Expression
Assertion	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$$