Theorem rabn0 3804

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 3803	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2813	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2739	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2810	. 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 367   E.wex 1617   e. wcel 1823   {cab 2439   =/= wne 2649   E.wrex 2805   {crab 2808   (/)c0 3783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-nul 3784

This theorem is referenced by:  rabeq0  3806  class2set  4604  reusv2  4643  exss  4700  frminex  4848  weniso  6225  onminesb  6606  onminsb  6607  onminex  6615  oeeulem  7242  supval2  7906  ordtypelem3  7937  card2on  7972  tz9.12lem3  8198  rankf  8203  scott0  8295  karden  8304  cardf2  8315  cardval3  8324  cardmin2  8370  acni3  8419  kmlem3  8523  cofsmo  8640  coftr  8644  fin23lem7  8687  enfin2i  8692  axcc4  8810  axdc3lem4  8824  ac6num  8850  pwfseqlem3  9027  wuncval  9109  wunccl  9111  tskmcl  9208  infm3  10497  nnwos  11150  zsupss  11172  zmin  11179  rpnnen1lem1  11209  rpnnen1lem2  11210  rpnnen1lem3  11211  rpnnen1lem5  11213  ioo0  11557  ico0  11578  ioc0  11579  icc0  11580  bitsfzolem  14171  odzcllem  14406  vdwnn  14603  ram0  14627  ramsey  14635  sylow2blem3  16844  iscyg2  17087  pgpfac1lem5  17328  ablfaclem2  17335  ablfaclem3  17336  ablfac  17337  lspf  17818  ordtrest2lem  19874  ordthauslem  20054  1stcfb  20115  2ndcdisj  20126  ptclsg  20285  txcon  20359  txflf  20676  tsmsfbas  20795  iscmet3  21901  minveclem3b  22012  iundisj  22127  dyadmax  22176  dyadmbllem  22177  elqaalem1  22884  elqaalem3  22886  sgmnncl  23622  musum  23668  uvtx01vtx  24697  spancl  26455  shsval2i  26506  ococin  26527  iundisjf  27662  iundisjfi  27838  ordtrest2NEWlem  28142  esumrnmpt2  28300  esumpinfval  28305  dmsigagen  28377  ballotlemfc0  28698  ballotlemfcc  28699  ballotlemiex  28707  ballotlemsup  28710  conpcon  28947  iscvm  28971  wsuclem  29624  nodenselem4  29687  sstotbnd2  30513  igenval  30701  igenidl  30703  pellfundre  31059  pellfundge  31060  pellfundglb  31063  dgraalem  31338  rgspncl  31362  lcmcllem  31446  ioodvbdlimc1lem1  31970  fourierdlem31  32162  fourierdlem64  32195  etransclem48  32307  bnj110  34336  bnj1204  34488  bnj1253  34493  pmap0  35905