Theorem class2set

Description: The class of elements of A "such that A is a set" is a set. That class is equal to A when A is a set (see class2seteq ) and to the empty set when A is a proper class. (Contributed by NM, 16-Oct-2003)

	Ref	Expression
Assertion	class2set	|- { x e. A | A e. _V } e. _V

Proof

Step	Hyp	Ref	Expression
1		rabexg	|- ( A e. _V -> { x e. A | A e. _V } e. _V )
2		simpl	|- ( ( -. A e. _V /\ x e. A ) -> -. A e. _V )
3	2	nrexdv	|- ( -. A e. _V -> -. E. x e. A A e. _V )
4		rabn0	|- ( { x e. A | A e. _V } =/= (/) <-> E. x e. A A e. _V )
5	4	necon1bbii	|- ( -. E. x e. A A e. _V <-> { x e. A | A e. _V } = (/) )
6	3 5	sylib	|- ( -. A e. _V -> { x e. A | A e. _V } = (/) )
7		0ex	|- (/) e. _V
8	6 7	eqeltrdi	|- ( -. A e. _V -> { x e. A | A e. _V } e. _V )
9	1 8	pm2.61i	|- { x e. A | A e. _V } e. _V