Theorem rabn0 3805

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 3804	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2823	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2752	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2820	. 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 1596   e. wcel 1767   {cab 2452   =/= wne 2662   E.wrex 2815   {crab 2818   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-nul 3786

This theorem is referenced by:  rabeq0  3807  class2set  4614  reusv2  4653  exss  4710  frminex  4859  weniso  6236  onminesb  6611  onminsb  6612  onminex  6620  oeeulem  7247  supval2  7911  ordtypelem3  7941  card2on  7976  tz9.12lem3  8203  rankf  8208  scott0  8300  karden  8309  cardf2  8320  cardval3  8329  cardmin2  8375  acni3  8424  kmlem3  8528  cofsmo  8645  coftr  8649  fin23lem7  8692  enfin2i  8697  axcc4  8815  axdc3lem4  8829  ac6num  8855  pwfseqlem3  9034  wuncval  9116  wunccl  9118  tskmcl  9215  infm3  10498  nnwos  11145  zsupss  11167  zmin  11174  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  ioo0  11550  ico0  11571  ioc0  11572  icc0  11573  bitsfzolem  13939  odzcllem  14174  vdwnn  14371  ram0  14395  ramsey  14403  sylow2blem3  16438  iscyg2  16676  pgpfac1lem5  16920  ablfaclem2  16927  ablfaclem3  16928  ablfac  16929  lspf  17403  ordtrest2lem  19470  ordthauslem  19650  1stcfb  19712  2ndcdisj  19723  ptclsg  19851  txcon  19925  txflf  20242  tsmsfbas  20361  iscmet3  21467  minveclem3b  21578  iundisj  21693  dyadmax  21742  dyadmbllem  21743  elqaalem1  22449  elqaalem3  22451  sgmnncl  23149  musum  23195  uvtx01vtx  24168  spancl  25930  shsval2i  25981  ococin  26002  iundisjf  27121  iundisjfi  27269  ordtrest2NEWlem  27540  esumpinfval  27719  dmsigagen  27784  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemiex  28080  ballotlemsup  28083  conpcon  28320  iscvm  28344  wsuclem  28958  nodenselem4  29021  sstotbnd2  29873  igenval  30061  igenidl  30063  pellfundre  30421  pellfundge  30422  pellfundglb  30425  dgraalem  30699  rgspncl  30723  lcmcllem  30802  ioodvbdlimc1lem1  31261  fourierdlem31  31438  fourierdlem45  31452  fourierdlem64  31471  bnj110  32995  bnj1204  33147  bnj1253  33152  pmap0  34561