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

Theorem rabn0 3805
Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.)
Assertion
Ref Expression
rabn0

Proof of Theorem rabn0
StepHypRef Expression
1 abn0 3804 . 2
2 df-rab 2816 . . 3
32neeq1i 2742 . 2
4 df-rex 2813 . 2
51, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  {cab 2442  =/=wne 2652  E.wrex 2808  {crab 2811   c0 3784
This theorem is referenced by:  rabeq0  3807  class2set  4619  reusv2  4658  exss  4715  frminex  4864  weniso  6250  onminesb  6633  onminsb  6634  onminex  6642  oeeulem  7269  supval2  7935  ordtypelem3  7966  card2on  8001  tz9.12lem3  8228  rankf  8233  scott0  8325  karden  8334  cardf2  8345  cardval3  8354  cardmin2  8400  acni3  8449  kmlem3  8553  cofsmo  8670  coftr  8674  fin23lem7  8717  enfin2i  8722  axcc4  8840  axdc3lem4  8854  ac6num  8880  pwfseqlem3  9059  wuncval  9141  wunccl  9143  tskmcl  9240  infm3  10527  nnwos  11178  zsupss  11200  zmin  11207  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  bitsfzolem  14084  odzcllem  14319  vdwnn  14516  ram0  14540  ramsey  14548  sylow2blem3  16642  iscyg2  16885  pgpfac1lem5  17130  ablfaclem2  17137  ablfaclem3  17138  ablfac  17139  lspf  17620  ordtrest2lem  19704  ordthauslem  19884  1stcfb  19946  2ndcdisj  19957  ptclsg  20116  txcon  20190  txflf  20507  tsmsfbas  20626  iscmet3  21732  minveclem3b  21843  iundisj  21958  dyadmax  22007  dyadmbllem  22008  elqaalem1  22715  elqaalem3  22717  sgmnncl  23421  musum  23467  uvtx01vtx  24492  spancl  26254  shsval2i  26305  ococin  26326  iundisjf  27448  iundisjfi  27601  ordtrest2NEWlem  27904  esumpinfval  28079  dmsigagen  28144  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  ballotlemsup  28443  conpcon  28680  iscvm  28704  wsuclem  29381  nodenselem4  29444  sstotbnd2  30270  igenval  30458  igenidl  30460  pellfundre  30817  pellfundge  30818  pellfundglb  30821  dgraalem  31094  rgspncl  31118  lcmcllem  31202  ioodvbdlimc1lem1  31728  fourierdlem31  31920  fourierdlem64  31953  etransclem48  32065  bnj110  33916  bnj1204  34068  bnj1253  34073  pmap0  35489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator