Theorem rabn0 3607

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

Step	Hyp	Ref	Expression
1		abn0 3606	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2675	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2577	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2672	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 269	1 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Syntax hints:   <-> wb 177   /\ wa 359   E.wex 1547   e. wcel 1721   {cab 2390   =/= wne 2567   E.wrex 2667   {crab 2670   (/)c0 3588

This theorem is referenced by:  rabeq0  3609  class2set  4327  exss  4386  frminex  4522  reusv2  4688  onminesb  4737  onminsb  4738  onminex  4746  weniso  6034  oeeulem  6803  ordtypelem3  7445  card2on  7478  tz9.12lem3  7671  rankf  7676  scott0  7766  karden  7775  cardf2  7786  cardval3  7795  cardmin2  7841  acni3  7884  kmlem3  7988  cofsmo  8105  coftr  8109  fin23lem7  8152  enfin2i  8157  axcc4  8275  axdc3lem4  8289  ac6num  8315  pwfseqlem3  8491  wuncval  8573  wunccl  8575  tskmcl  8672  infm3  9923  nnwos  10500  zsupss  10521  zmin  10526  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  bitsfzolem  12901  odzcllem  13133  vdwnn  13321  ram0  13345  ramsey  13353  sylow2blem3  15211  iscyg2  15447  pgpfac1lem5  15592  ablfaclem2  15599  ablfaclem3  15600  ablfac  15601  lspf  16005  ordtrest2lem  17221  ordthauslem  17401  1stcfb  17461  2ndcdisj  17472  ptclsg  17600  txcon  17674  txflf  17991  tsmsfbas  18110  iscmet3  19199  minveclem3b  19282  iundisj  19395  dyadmax  19443  dyadmbllem  19444  elqaalem1  20189  elqaalem3  20191  sgmnncl  20883  musum  20929  uvtx01vtx  21454  spancl  22791  shsval2i  22842  ococin  22863  iundisjf  23982  iundisjfi  24105  esumpinfval  24416  dmsigagen  24480  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemiex  24712  ballotlemsup  24715  conpcon  24875  iscvm  24899  nodenselem4  25552  sstotbnd2  26373  igenval  26561  igenidl  26563  pellfundre  26834  pellfundge  26835  pellfundglb  26838  dgraalem  27218  rgspncl  27242  bnj110  28935  bnj1204  29087  bnj1253  29092  pmap0  30247

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-nul 3589