Theorem class2set

Description: Construct, from any class A , a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists. (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