Theorem rabn0 3788

Description: Nonempty 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 3787	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2791	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2716	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2788	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 280	1 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Syntax hints:   <-> wb 187   /\ wa 370   E.wex 1659   e. wcel 1870   {cab 2414   =/= wne 2625   E.wrex 2783   {crab 2786   (/)c0 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-nul 3768

This theorem is referenced by:  rabeq0  3790  class2set  4592  reusv2  4631  exss  4685  frminex  4834  weniso  6260  onminesb  6639  onminsb  6640  onminex  6648  oeeulem  7310  supval2  7975  ordtypelem3  8035  card2on  8069  tz9.12lem3  8259  rankf  8264  scott0  8356  karden  8365  cardf2  8376  cardval3  8385  cardmin2  8431  acni3  8476  kmlem3  8580  cofsmo  8697  coftr  8701  fin23lem7  8744  enfin2i  8749  axcc4  8867  axdc3lem4  8881  ac6num  8907  pwfseqlem3  9084  wuncval  9166  wunccl  9168  tskmcl  9265  infm3  10568  nnwos  11226  zsupss  11253  zmin  11260  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  bitsfzolem  14382  lcmcllem  14532  lcmscllemOLD  14553  fissn0dvdsn0  14561  odzcllem  14706  vdwnn  14911  ram0  14943  ramsey  14951  sylow2blem3  17209  iscyg2  17452  pgpfac1lem5  17647  ablfaclem2  17654  ablfaclem3  17655  ablfac  17656  lspf  18132  ordtrest2lem  20150  ordthauslem  20330  1stcfb  20391  2ndcdisj  20402  ptclsg  20561  txcon  20635  txflf  20952  tsmsfbas  21073  iscmet3  22156  minveclem3b  22263  iundisj  22378  dyadmax  22433  dyadmbllem  22434  elqaalem1  23140  elqaalem3  23142  sgmnncl  23937  musum  23983  uvtx01vtx  25065  spancl  26824  shsval2i  26875  ococin  26896  iundisjf  28038  iundisjfi  28208  ordtrest2NEWlem  28567  esumrnmpt2  28728  esumpinfval  28733  dmsigagen  28805  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemiex  29160  ballotlemsup  29163  bnj110  29457  bnj1204  29609  bnj1253  29614  conpcon  29746  iscvm  29770  wsuclem  30295  nodenselem4  30358  poimirlem28  31671  sstotbnd2  31809  igenval  31997  igenidl  31999  pmap0  33038  pellfundre  35434  pellfundge  35435  pellfundglb  35438  dgraalem  35709  rgspncl  35733  uzwo4  37032  ioodvbdlimc1lem1  37374  fourierdlem31  37568  fourierdlem64  37601  etransclem48  37713