MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabn0 Structured version   Unicode version

Theorem rabn0 3639
Description: Non-empty 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
StepHypRef Expression
1 abn0 3638 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  =/=  (/)  <->  E. x
( x  e.  A  /\  ph ) )
2 df-rab 2706 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
32neeq1i 2608 . 2  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  { x  |  ( x  e.  A  /\  ph ) }  =/=  (/) )
4 df-rex 2703 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
51, 3, 43bitr4i 269 1  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550    e. wcel 1725   {cab 2421    =/= wne 2598   E.wrex 2698   {crab 2701   (/)c0 3620
This theorem is referenced by:  rabeq0  3641  class2set  4359  exss  4418  frminex  4554  reusv2  4721  onminesb  4770  onminsb  4771  onminex  4779  weniso  6067  oeeulem  6836  ordtypelem3  7479  card2on  7512  tz9.12lem3  7705  rankf  7710  scott0  7800  karden  7809  cardf2  7820  cardval3  7829  cardmin2  7875  acni3  7918  kmlem3  8022  cofsmo  8139  coftr  8143  fin23lem7  8186  enfin2i  8191  axcc4  8309  axdc3lem4  8323  ac6num  8349  pwfseqlem3  8525  wuncval  8607  wunccl  8609  tskmcl  8706  infm3  9957  nnwos  10534  zsupss  10555  zmin  10560  rpnnen1lem1  10590  rpnnen1lem2  10591  rpnnen1lem3  10592  rpnnen1lem5  10594  ioo0  10931  ico0  10952  ioc0  10953  icc0  10954  bitsfzolem  12936  odzcllem  13168  vdwnn  13356  ram0  13380  ramsey  13388  sylow2blem3  15246  iscyg2  15482  pgpfac1lem5  15627  ablfaclem2  15634  ablfaclem3  15635  ablfac  15636  lspf  16040  ordtrest2lem  17257  ordthauslem  17437  1stcfb  17498  2ndcdisj  17509  ptclsg  17637  txcon  17711  txflf  18028  tsmsfbas  18147  iscmet3  19236  minveclem3b  19319  iundisj  19432  dyadmax  19480  dyadmbllem  19481  elqaalem1  20226  elqaalem3  20228  sgmnncl  20920  musum  20966  uvtx01vtx  21491  spancl  22828  shsval2i  22879  ococin  22900  iundisjf  24019  iundisjfi  24142  esumpinfval  24453  dmsigagen  24517  ballotlemfc0  24740  ballotlemfcc  24741  ballotlemiex  24749  ballotlemsup  24752  conpcon  24912  iscvm  24936  nodenselem4  25604  sstotbnd2  26437  igenval  26625  igenidl  26627  pellfundre  26898  pellfundge  26899  pellfundglb  26902  dgraalem  27282  rgspncl  27306  bnj110  29130  bnj1204  29282  bnj1253  29287  pmap0  30463
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator