Theorem issetri

Description: A way to say " A is a set" (inference form). (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	issetri.1	$$⊢\exists xx=A$$
Assertion	issetri	$$⊢A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		issetri.1	$$⊢\exists xx=A$$
2		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
3	1 2	mpbir	$$⊢A\in \mathrm{V}$$