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

Theorem rabn0 3474
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 3473 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  =/=  (/)  <->  E. x
( x  e.  A  /\  ph ) )
2 df-rab 2552 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
32neeq1i 2456 . 2  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  { x  |  ( x  e.  A  /\  ph ) }  =/=  (/) )
4 df-rex 2549 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
51, 3, 43bitr4i 268 1  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    e. wcel 1684   {cab 2269    =/= wne 2446   E.wrex 2544   {crab 2547   (/)c0 3455
This theorem is referenced by:  rabeq0  3476  class2set  4178  exss  4236  frminex  4373  reusv2  4540  onminesb  4589  onminsb  4590  onminex  4598  weniso  5852  oeeulem  6599  ordtypelem3  7235  card2on  7268  tz9.12lem3  7461  rankf  7466  scott0  7556  karden  7565  cardf2  7576  cardval3  7585  cardmin2  7631  acni3  7674  kmlem3  7778  cofsmo  7895  coftr  7899  fin23lem7  7942  enfin2i  7947  axcc4  8065  axdc3lem4  8079  ac6num  8106  pwfseqlem3  8282  wuncval  8364  wunccl  8366  tskmcl  8463  infm3  9713  nnwos  10286  zsupss  10307  zmin  10312  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  bitsfzolem  12625  odzcllem  12857  vdwnn  13045  ram0  13069  ramsey  13077  sylow2blem3  14933  iscyg2  15169  pgpfac1lem5  15314  ablfaclem2  15321  ablfaclem3  15322  ablfac  15323  lspf  15731  ordtrest2lem  16933  ordthauslem  17111  1stcfb  17171  2ndcdisj  17182  ptclsg  17309  txcon  17383  txflf  17701  tsmsfbas  17810  iscmet3  18719  minveclem3b  18792  iundisj  18905  dyadmax  18953  dyadmbllem  18954  elqaalem1  19699  elqaalem3  19701  sgmnncl  20385  musum  20431  spancl  21915  shsval2i  21966  ococin  21987  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemiex  23060  ballotlemsup  23063  iundisjfi  23363  iundisjf  23365  esumpinfval  23441  dmsigagen  23505  conpcon  23766  iscvm  23790  nodenselem4  24338  dstr  25171  istopx  25547  nbssntrs  26147  sstotbnd2  26498  igenval  26686  igenidl  26688  pellfundre  26966  pellfundge  26967  pellfundglb  26970  dgraalem  27350  rgspncl  27374  uvtx01vtx  28164  bnj110  28890  bnj1204  29042  bnj1253  29047  pmap0  29954
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator