Theorem issetri

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

	Ref	Expression
Hypothesis	issetri.1	|- E. x x = A
Assertion	issetri	|- A e. _V

Proof

Step	Hyp	Ref	Expression
1		issetri.1	|- E. x x = A
2		isset	|- ( A e. _V <-> E. x x = A )
3	1 2	mpbir	|- A e. _V