Theorem rabn0 3752

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 3751	. 2 |- ( { x | ( x e. A /\ ph ) } =/= (/) <-> E. x ( x e. A /\ ph ) )
2		df-rab 2746	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3	2	neeq1i 2688	. 2 |- ( { x e. A | ph } =/= (/) <-> { x | ( x e. A /\ ph ) } =/= (/) )
4		df-rex 2743	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	1, 3, 4	3bitr4i 281	1 |- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Syntax hints:   <-> wb 188   /\ wa 371   E.wex 1663   e. wcel 1887   {cab 2437   =/= wne 2622   E.wrex 2738   {crab 2741   (/)c0 3731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-nul 3732

This theorem is referenced by:  rabeq0  3754  class2set  4570  reusv2  4609  exss  4663  frminex  4814  weniso  6245  onminesb  6625  onminsb  6626  onminex  6634  oeeulem  7302  supval2  7969  ordtypelem3  8035  card2on  8069  tz9.12lem3  8260  rankf  8265  scott0  8357  karden  8366  cardf2  8377  cardval3  8386  cardmin2  8432  acni3  8478  kmlem3  8582  cofsmo  8699  coftr  8703  fin23lem7  8746  enfin2i  8751  axcc4  8869  axdc3lem4  8883  ac6num  8909  pwfseqlem3  9085  wuncval  9167  wunccl  9169  tskmcl  9266  infm3  10568  nnwos  11226  zsupss  11253  zmin  11260  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  bitsfzolem  14407  bitsfzolemOLD  14408  lcmcllem  14561  lcmscllemOLD  14582  fissn0dvdsn0  14590  odzcllem  14737  odzcllemOLD  14743  vdwnn  14948  ram0  14980  ramsey  14988  sylow2blem3  17274  iscyg2  17517  pgpfac1lem5  17712  ablfaclem2  17719  ablfaclem3  17720  ablfac  17721  lspf  18197  ordtrest2lem  20219  ordthauslem  20399  1stcfb  20460  2ndcdisj  20471  ptclsg  20630  txcon  20704  txflf  21021  tsmsfbas  21142  iscmet3  22263  minveclem3b  22370  minveclem3bOLD  22382  iundisj  22501  dyadmax  22556  dyadmbllem  22557  elqaalem1  23272  elqaalem3  23274  elqaalem1OLD  23275  elqaalem3OLD  23277  sgmnncl  24074  musum  24120  uvtx01vtx  25220  spancl  26989  shsval2i  27040  ococin  27061  iundisjf  28199  iundisjfi  28372  ordtrest2NEWlem  28728  esumrnmpt2  28889  esumpinfval  28894  dmsigagen  28966  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemiex  29334  ballotlemsup  29337  ballotlemiexOLD  29372  ballotlemsupOLD  29375  bnj110  29669  bnj1204  29821  bnj1253  29826  conpcon  29958  iscvm  29982  wsuclem  30508  nodenselem4  30573  poimirlem28  31968  sstotbnd2  32106  igenval  32294  igenidl  32296  pmap0  33330  pellfundre  35729  pellfundge  35730  pellfundglb  35733  dgraalem  36007  dgraalemOLD  36008  rgspncl  36035  uzwo4  37392  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem1OLD  37805  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem64  38034  etransclem48OLD  38147  etransclem48  38148  incistruhgr  39171  uvtxa01vtx0  39469