This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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