Theorem elisset

Description: An element of a class exists. (Contributed by NM, 1-May-1995) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019)

	Ref	Expression
Assertion	elisset	$$⊢A\in V\to \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		exsimpl	$$⊢\exists y\left(y=A\wedge y\in V\right)\to \exists yy=A$$
2		dfclel	$$⊢A\in V\leftrightarrow \exists y\left(y=A\wedge y\in V\right)$$
3		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
4	3	cbvexvw	$$⊢\exists xx=A\leftrightarrow \exists yy=A$$
5	1 2 4	3imtr4i	$$⊢A\in V\to \exists xx=A$$