Theorem elisset

Description: An element of a class exists. Use elissetv instead when sufficient (for instance in usages where x is a dummy variable). (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		elissetv	$$⊢A\in V\to \exists yy=A$$
2		vextru	$$⊢y\in \left\{z|\top \right\}$$
3	2	biantru	$$⊢y=A\leftrightarrow \left(y=A\wedge y\in \left\{z|\top \right\}\right)$$
4	3	exbii	$$⊢\exists yy=A\leftrightarrow \exists y\left(y=A\wedge y\in \left\{z|\top \right\}\right)$$
5		dfclel	$$⊢A\in \left\{z|\top \right\}\leftrightarrow \exists y\left(y=A\wedge y\in \left\{z|\top \right\}\right)$$
6	4 5	bitr4i	$$⊢\exists yy=A\leftrightarrow A\in \left\{z|\top \right\}$$
7		vextru	$$⊢x\in \left\{z|\top \right\}$$
8	7	biantru	$$⊢x=A\leftrightarrow \left(x=A\wedge x\in \left\{z|\top \right\}\right)$$
9	8	exbii	$$⊢\exists xx=A\leftrightarrow \exists x\left(x=A\wedge x\in \left\{z|\top \right\}\right)$$
10		dfclel	$$⊢A\in \left\{z|\top \right\}\leftrightarrow \exists x\left(x=A\wedge x\in \left\{z|\top \right\}\right)$$
11	9 10	bitr4i	$$⊢\exists xx=A\leftrightarrow A\in \left\{z|\top \right\}$$
12	6 11	bitr4i	$$⊢\exists yy=A\leftrightarrow \exists xx=A$$
13	1 12	sylib	$$⊢A\in V\to \exists xx=A$$