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

Theorem rabn0 3592
Description: Non-empty restricted class abstraction. (Contributed by NM, 29-Aug-1999.)
Assertion
Ref Expression
rabn0  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )

Proof of Theorem rabn0
StepHypRef Expression
1 abn0 3591 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  =/=  (/)  <->  E. x
( x  e.  A  /\  ph ) )
2 df-rab 2660 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
32neeq1i 2562 . 2  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  { x  |  ( x  e.  A  /\  ph ) }  =/=  (/) )
4 df-rex 2657 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
51, 3, 43bitr4i 269 1  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    e. wcel 1717   {cab 2375    =/= wne 2552   E.wrex 2652   {crab 2655   (/)c0 3573
This theorem is referenced by:  rabeq0  3594  class2set  4310  exss  4369  frminex  4505  reusv2  4671  onminesb  4720  onminsb  4721  onminex  4729  weniso  6016  oeeulem  6782  ordtypelem3  7424  card2on  7457  tz9.12lem3  7650  rankf  7655  scott0  7745  karden  7754  cardf2  7765  cardval3  7774  cardmin2  7820  acni3  7863  kmlem3  7967  cofsmo  8084  coftr  8088  fin23lem7  8131  enfin2i  8136  axcc4  8254  axdc3lem4  8268  ac6num  8294  pwfseqlem3  8470  wuncval  8552  wunccl  8554  tskmcl  8651  infm3  9901  nnwos  10478  zsupss  10499  zmin  10504  rpnnen1lem1  10534  rpnnen1lem2  10535  rpnnen1lem3  10536  rpnnen1lem5  10538  ioo0  10875  ico0  10896  ioc0  10897  icc0  10898  bitsfzolem  12875  odzcllem  13107  vdwnn  13295  ram0  13319  ramsey  13327  sylow2blem3  15185  iscyg2  15421  pgpfac1lem5  15566  ablfaclem2  15573  ablfaclem3  15574  ablfac  15575  lspf  15979  ordtrest2lem  17191  ordthauslem  17371  1stcfb  17431  2ndcdisj  17442  ptclsg  17570  txcon  17644  txflf  17961  tsmsfbas  18080  iscmet3  19119  minveclem3b  19198  iundisj  19311  dyadmax  19359  dyadmbllem  19360  elqaalem1  20105  elqaalem3  20107  sgmnncl  20799  musum  20845  uvtx01vtx  21369  spancl  22688  shsval2i  22739  ococin  22760  iundisjf  23874  iundisjfi  23992  esumpinfval  24261  dmsigagen  24325  ballotlemfc0  24531  ballotlemfcc  24532  ballotlemiex  24540  ballotlemsup  24543  conpcon  24703  iscvm  24727  nodenselem4  25364  sstotbnd2  26176  igenval  26364  igenidl  26366  pellfundre  26637  pellfundge  26638  pellfundglb  26641  dgraalem  27021  rgspncl  27045  bnj110  28569  bnj1204  28721  bnj1253  28726  pmap0  29881
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-nul 3574
  Copyright terms: Public domain W3C validator