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

Theorem rabn0 3487
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 3486 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  =/=  (/)  <->  E. x
( x  e.  A  /\  ph ) )
2 df-rab 2565 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
32neeq1i 2469 . 2  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  { x  |  ( x  e.  A  /\  ph ) }  =/=  (/) )
4 df-rex 2562 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
51, 3, 43bitr4i 268 1  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531    e. wcel 1696   {cab 2282    =/= wne 2459   E.wrex 2557   {crab 2560   (/)c0 3468
This theorem is referenced by:  rabeq0  3489  class2set  4194  exss  4252  frminex  4389  reusv2  4556  onminesb  4605  onminsb  4606  onminex  4614  weniso  5868  oeeulem  6615  ordtypelem3  7251  card2on  7284  tz9.12lem3  7477  rankf  7482  scott0  7572  karden  7581  cardf2  7592  cardval3  7601  cardmin2  7647  acni3  7690  kmlem3  7794  cofsmo  7911  coftr  7915  fin23lem7  7958  enfin2i  7963  axcc4  8081  axdc3lem4  8095  ac6num  8122  pwfseqlem3  8298  wuncval  8380  wunccl  8382  tskmcl  8479  infm3  9729  nnwos  10302  zsupss  10323  zmin  10328  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  bitsfzolem  12641  odzcllem  12873  vdwnn  13061  ram0  13085  ramsey  13093  sylow2blem3  14949  iscyg2  15185  pgpfac1lem5  15330  ablfaclem2  15337  ablfaclem3  15338  ablfac  15339  lspf  15747  ordtrest2lem  16949  ordthauslem  17127  1stcfb  17187  2ndcdisj  17198  ptclsg  17325  txcon  17399  txflf  17717  tsmsfbas  17826  iscmet3  18735  minveclem3b  18808  iundisj  18921  dyadmax  18969  dyadmbllem  18970  elqaalem1  19715  elqaalem3  19717  sgmnncl  20401  musum  20447  spancl  21931  shsval2i  21982  ococin  22003  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemiex  23076  ballotlemsup  23079  iundisjfi  23378  iundisjf  23380  esumpinfval  23456  dmsigagen  23520  conpcon  23781  iscvm  23805  nodenselem4  24409  dstr  25274  istopx  25650  nbssntrs  26250  sstotbnd2  26601  igenval  26789  igenidl  26791  pellfundre  27069  pellfundge  27070  pellfundglb  27073  dgraalem  27453  rgspncl  27477  uvtx01vtx  28305  bnj110  29206  bnj1204  29358  bnj1253  29363  pmap0  30576
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator