Theorem issetid

Description: Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	issetid	$$⊢A\in \mathrm{V}\leftrightarrow A\mathrm{I}A$$

Proof

Step	Hyp	Ref	Expression
1		ididg	$$⊢A\in \mathrm{V}\to A\mathrm{I}A$$
2		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
3	2	brrelex1i	$$⊢A\mathrm{I}A\to A\in \mathrm{V}$$
4	1 3	impbii	$$⊢A\in \mathrm{V}\leftrightarrow A\mathrm{I}A$$