Theorem issetlem

Description: Lemma for elisset and isset . (Contributed by NM, 26-May-1993) Extract from the proof of isset . (Revised by WL, 2-Feb-2025)

	Ref	Expression
Hypothesis	issetlem.1	$$⊢x\in V$$
Assertion	issetlem	$$⊢A\in V\leftrightarrow \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		issetlem.1	$$⊢x\in V$$
2		dfclel	$$⊢A\in V\leftrightarrow \exists x\left(x=A\wedge x\in V\right)$$
3	1	biantru	$$⊢x=A\leftrightarrow \left(x=A\wedge x\in V\right)$$
4	3	exbii	$$⊢\exists xx=A\leftrightarrow \exists x\left(x=A\wedge x\in V\right)$$
5	2 4	bitr4i	$$⊢A\in V\leftrightarrow \exists xx=A$$