Theorem rabn0 3662

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 3661	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2729	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2623	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2726	. 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 1586   e. wcel 1756   {cab 2429   =/= wne 2611   E.wrex 2721   {crab 2724   (/)c0 3642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-nul 3643

This theorem is referenced by:  rabeq0  3664  class2set  4464  reusv2  4503  exss  4560  frminex  4705  weniso  6050  onminesb  6414  onminsb  6415  onminex  6423  oeeulem  7045  supval2  7710  ordtypelem3  7739  card2on  7774  tz9.12lem3  8001  rankf  8006  scott0  8098  karden  8107  cardf2  8118  cardval3  8127  cardmin2  8173  acni3  8222  kmlem3  8326  cofsmo  8443  coftr  8447  fin23lem7  8490  enfin2i  8495  axcc4  8613  axdc3lem4  8627  ac6num  8653  pwfseqlem3  8832  wuncval  8914  wunccl  8916  tskmcl  9013  infm3  10294  nnwos  10927  zsupss  10949  zmin  10954  rpnnen1lem1  10984  rpnnen1lem2  10985  rpnnen1lem3  10986  rpnnen1lem5  10988  ioo0  11330  ico0  11351  ioc0  11352  icc0  11353  bitsfzolem  13635  odzcllem  13869  vdwnn  14064  ram0  14088  ramsey  14096  sylow2blem3  16126  iscyg2  16364  pgpfac1lem5  16585  ablfaclem2  16592  ablfaclem3  16593  ablfac  16594  lspf  17060  ordtrest2lem  18812  ordthauslem  18992  1stcfb  19054  2ndcdisj  19065  ptclsg  19193  txcon  19267  txflf  19584  tsmsfbas  19703  iscmet3  20809  minveclem3b  20920  iundisj  21034  dyadmax  21083  dyadmbllem  21084  elqaalem1  21790  elqaalem3  21792  sgmnncl  22490  musum  22536  uvtx01vtx  23405  spancl  24744  shsval2i  24795  ococin  24816  iundisjf  25936  iundisjfi  26085  ordtrest2NEWlem  26357  esumpinfval  26527  dmsigagen  26592  ballotlemfc0  26880  ballotlemfcc  26881  ballotlemiex  26889  ballotlemsup  26892  conpcon  27129  iscvm  27153  wsuclem  27767  nodenselem4  27830  sstotbnd2  28678  igenval  28866  igenidl  28868  pellfundre  29227  pellfundge  29228  pellfundglb  29231  dgraalem  29507  rgspncl  29531  bnj110  31856  bnj1204  32008  bnj1253  32013  pmap0  33414