Theorem rabn0 3755

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 3754	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2765	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2707	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2762	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 285	1 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Syntax hints:   <-> wb 189   /\ wa 376   E.wex 1671   e. wcel 1904   {cab 2457   =/= wne 2641   E.wrex 2757   {crab 2760   (/)c0 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-nul 3723

This theorem is referenced by:  rabeq0  3757  class2set  4568  reusv2  4607  exss  4663  frminex  4819  weniso  6263  onminesb  6644  onminsb  6645  onminex  6653  oeeulem  7320  supval2  7987  ordtypelem3  8053  card2on  8087  tz9.12lem3  8278  rankf  8283  scott0  8375  karden  8384  cardf2  8395  cardval3  8404  cardmin2  8450  acni3  8496  kmlem3  8600  cofsmo  8717  coftr  8721  fin23lem7  8764  enfin2i  8769  axcc4  8887  axdc3lem4  8901  ac6num  8927  pwfseqlem3  9103  wuncval  9185  wunccl  9187  tskmcl  9284  infm3  10590  nnwos  11249  zsupss  11276  zmin  11283  rpnnen1lem1  11313  rpnnen1lem2  11314  rpnnen1lem3  11315  rpnnen1lem5  11317  ioo0  11686  ico0  11707  ioc0  11708  icc0  11709  bitsfzolem  14486  bitsfzolemOLD  14487  lcmcllem  14640  lcmscllemOLD  14661  fissn0dvdsn0  14669  odzcllem  14816  odzcllemOLD  14822  vdwnn  15027  ram0  15059  ramsey  15067  sylow2blem3  17352  iscyg2  17595  pgpfac1lem5  17790  ablfaclem2  17797  ablfaclem3  17798  ablfac  17799  lspf  18275  ordtrest2lem  20296  ordthauslem  20476  1stcfb  20537  2ndcdisj  20548  ptclsg  20707  txcon  20781  txflf  21099  tsmsfbas  21220  iscmet3  22341  minveclem3b  22448  minveclem3bOLD  22460  iundisj  22580  dyadmax  22635  dyadmbllem  22636  elqaalem1  23351  elqaalem3  23353  elqaalem1OLD  23354  elqaalem3OLD  23356  sgmnncl  24153  musum  24199  uvtx01vtx  25299  spancl  27070  shsval2i  27121  ococin  27142  iundisjf  28276  iundisjfi  28447  ordtrest2NEWlem  28802  esumrnmpt2  28963  esumpinfval  28968  dmsigagen  29040  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemiex  29407  ballotlemsup  29410  ballotlemiexOLD  29445  ballotlemsupOLD  29448  bnj110  29741  bnj1204  29893  bnj1253  29898  conpcon  30030  iscvm  30054  wsuclem  30579  nodenselem4  30644  poimirlem28  32032  sstotbnd2  32170  igenval  32358  igenidl  32360  pmap0  33401  pellfundre  35800  pellfundge  35801  pellfundglb  35804  dgraalem  36078  dgraalemOLD  36079  rgspncl  36106  uzwo4  37451  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem1OLD  37902  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem64  38146  etransclem48OLD  38259  etransclem48  38260  incistruhgr  39325  uvtxa01vtx0  39633