MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  class2set Unicode version

Theorem class2set 4150
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.)
Assertion
Ref Expression
class2set  |-  { x  e.  A  |  A  e.  _V }  e.  _V
Distinct variable group:    x, A

Proof of Theorem class2set
StepHypRef Expression
1 rabexg 4138 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  A  e.  _V }  e.  _V )
2 simpl 445 . . . . 5  |-  ( ( -.  A  e.  _V  /\  x  e.  A )  ->  -.  A  e.  _V )
32nrexdv 2621 . . . 4  |-  ( -.  A  e.  _V  ->  -. 
E. x  e.  A  A  e.  _V )
4 rabn0 3449 . . . . 5  |-  ( { x  e.  A  |  A  e.  _V }  =/=  (/)  <->  E. x  e.  A  A  e.  _V )
54necon1bbii 2473 . . . 4  |-  ( -. 
E. x  e.  A  A  e.  _V  <->  { x  e.  A  |  A  e.  _V }  =  (/) )
63, 5sylib 190 . . 3  |-  ( -.  A  e.  _V  ->  { x  e.  A  |  A  e.  _V }  =  (/) )
7 0ex 4124 . . 3  |-  (/)  e.  _V
86, 7syl6eqel 2346 . 2  |-  ( -.  A  e.  _V  ->  { x  e.  A  |  A  e.  _V }  e.  _V )
91, 8pm2.61i 158 1  |-  { x  e.  A  |  A  e.  _V }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    = wceq 1619    e. wcel 1621   E.wrex 2519   {crab 2522   _Vcvv 2763   (/)c0 3430
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator