Theorem rabn0 3645

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 3644	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2714	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2608	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2711	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 277	1 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Syntax hints:   <-> wb 184   /\ wa 369   E.wex 1589   e. wcel 1755   {cab 2419   =/= wne 2596   E.wrex 2706   {crab 2709   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  rabeq0  3647  class2set  4447  reusv2  4486  exss  4543  frminex  4687  weniso  6032  onminesb  6398  onminsb  6399  onminex  6407  oeeulem  7028  supval2  7693  ordtypelem3  7722  card2on  7757  tz9.12lem3  7984  rankf  7989  scott0  8081  karden  8090  cardf2  8101  cardval3  8110  cardmin2  8156  acni3  8205  kmlem3  8309  cofsmo  8426  coftr  8430  fin23lem7  8473  enfin2i  8478  axcc4  8596  axdc3lem4  8610  ac6num  8636  pwfseqlem3  8814  wuncval  8896  wunccl  8898  tskmcl  8995  infm3  10276  nnwos  10909  zsupss  10931  zmin  10936  rpnnen1lem1  10966  rpnnen1lem2  10967  rpnnen1lem3  10968  rpnnen1lem5  10970  ioo0  11312  ico0  11333  ioc0  11334  icc0  11335  bitsfzolem  13612  odzcllem  13846  vdwnn  14041  ram0  14065  ramsey  14073  sylow2blem3  16100  iscyg2  16338  pgpfac1lem5  16553  ablfaclem2  16560  ablfaclem3  16561  ablfac  16562  lspf  16976  ordtrest2lem  18648  ordthauslem  18828  1stcfb  18890  2ndcdisj  18901  ptclsg  19029  txcon  19103  txflf  19420  tsmsfbas  19539  iscmet3  20645  minveclem3b  20756  iundisj  20870  dyadmax  20919  dyadmbllem  20920  elqaalem1  21669  elqaalem3  21671  sgmnncl  22369  musum  22415  uvtx01vtx  23222  spancl  24561  shsval2i  24612  ococin  24633  iundisjf  25754  iundisjfi  25902  ordtrest2NEWlem  26205  esumpinfval  26375  dmsigagen  26440  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemiex  26731  ballotlemsup  26734  conpcon  26971  iscvm  26995  wsuclem  27608  nodenselem4  27671  sstotbnd2  28514  igenval  28702  igenidl  28704  pellfundre  29064  pellfundge  29065  pellfundglb  29068  dgraalem  29344  rgspncl  29368  bnj110  31550  bnj1204  31702  bnj1253  31707  pmap0  32979