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

Theorem n0 3498
Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
n0  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Distinct variable group:    x, A

Proof of Theorem n0
StepHypRef Expression
1 nfcv 2452 . 2  |-  F/_ x A
21n0f 3497 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1532    e. wcel 1701    =/= wne 2479   (/)c0 3489
This theorem is referenced by:  neq0  3499  reximdva0  3500  n0moeu  3501  pssnel  3553  r19.2z  3577  r19.2zb  3578  r19.3rz  3579  r19.3rzv  3581  uniintsn  3936  iunn0  3999  trint0  4167  intex  4204  notzfaus  4222  nnullss  4272  exss  4273  opabn0  4332  wefrc  4424  wereu2  4427  onfr  4468  reusv2lem1  4572  reusv5OLD  4581  limuni3  4680  dmxp  4934  xpnz  5136  soex  5159  dmsnn0  5175  unixp0  5243  isofrlem  5879  f1oweALT  5893  fo1stres  6185  fo2ndres  6186  ecdmn0  6744  map0g  6850  ixpn0  6891  resixpfo  6897  domdifsn  6988  xpdom3  7003  fodomr  7055  mapdom3  7076  findcard2  7143  unblem2  7155  marypha1lem  7231  brwdom2  7332  unxpwdom2  7347  ixpiunwdom  7350  zfreg  7354  zfreg2  7355  epfrs  7458  scott0  7601  cplem1  7604  fseqen  7699  finacn  7722  iunfictbso  7786  aceq2  7791  dfac3  7793  dfac9  7807  kmlem6  7826  kmlem8  7828  infpss  7888  fin23lem7  7987  enfin2i  7992  fin23lem21  8010  fin23lem31  8014  isf32lem9  8032  isf34lem4  8048  axdc2lem  8119  axdc3lem4  8124  ac6c4  8153  ac9  8155  ac6s4  8162  ac9s  8165  ttukeyg  8189  fpwwe2lem12  8308  wun0  8385  tsk0  8430  gruina  8485  genpn0  8672  prlem934  8702  ltaddpr  8703  ltexprlem1  8705  prlem936  8716  reclem2pr  8717  suplem1pr  8721  supsr  8779  axpre-sup  8836  infm3  9758  supmul1  9764  supmullem2  9766  supmul  9767  infmrcl  9778  negn0  10351  zsupss  10354  xrsupsslem  10672  xrinfmsslem  10673  supxrre  10693  infmxrre  10701  ixxub  10724  ixxlb  10725  ioorebas  10792  fzn0  10856  fzon0  10938  swrdcl  11499  maxprmfct  12839  4sqlem12  13050  vdwmc  13072  ramz  13119  ramub1  13122  mreiincl  13547  mremre  13555  mreexexlem4d  13598  iscatd2  13632  drsdirfi  14121  issubg2  14685  subgint  14690  giclcl  14785  gicrcl  14786  gicsym  14787  gictr  14788  gicen  14790  gicsubgen  14791  cntzssv  14853  sylow1lem4  14961  odcau  14964  sylow3  14993  cyggex2  15232  giccyg  15235  pgpfac1lem5  15363  subrgint  15616  lss0cl  15753  lmiclcl  15872  lmicrcl  15873  lmicsym  15874  lspsnat  15947  lspprat  15955  abvn0b  16092  cnsubrg  16488  cygzn  16580  toponmre  16886  iunconlem  17209  iuncon  17210  uncon  17211  clscon  17212  2ndcdisj  17238  2ndcsep  17241  1stcelcls  17243  txcls  17355  hmphsym  17529  hmphtr  17530  hmphen  17532  haushmphlem  17534  cmphmph  17535  conhmph  17536  reghmph  17540  nrmhmph  17541  hmphdis  17543  hmphen2  17546  fbdmn0  17581  isfbas2  17582  fbssint  17585  trfbas2  17590  filtop  17602  isfil2  17603  elfg  17618  fgcl  17625  filssufilg  17658  uffix2  17671  ufildom1  17673  hauspwpwf1  17734  hausflf2  17745  alexsubALTlem2  17794  ptcmplem2  17799  tgptsmscld  17885  xbln0  18017  lpbl  18101  met2ndci  18120  reconn  18385  opnreen  18388  metdsre  18409  phtpcer  18546  phtpc01  18547  phtpcco2  18550  pcohtpy  18571  cfilfcls  18753  cmetcaulem  18767  cmetcau  18768  cmetss  18793  bcthlem5  18803  ovolicc2lem2  18930  ovolicc2lem5  18933  ioorcl2  18980  ioorinv2  18983  itg11  19099  dvlip  19393  dvne0  19411  mpfrcl  19455  fta1g  19606  plyssc  19635  fta1  19741  vieta1lem2  19744  isgrp2d  20955  ubthlem1  21504  shintcli  21963  fmcncfil  23386  ustfilxp  23429  xpco  23434  metustfbas  23499  restmetu  23513  esumcst  23631  insiga  23696  pconcon  24046  txscon  24056  cvmsss2  24089  cvmopnlem  24093  cvmfolem  24094  cvmliftmolem2  24097  cvmlift2lem10  24127  cvmliftpht  24133  cvmlift3lem8  24141  umgraex  24159  eupath  24189  dedekind  24368  dedekindle  24369  eldm3  24504  fundmpss  24507  frmin  24627  nocvxmin  24730  axcontlem4  24981  axcontlem10  24987  supaddc  25309  supadd  25310  itg2addnclem2  25318  locfincmp  25453  comppfsc  25456  neibastop1  25457  neibastop2lem  25458  neibastop2  25459  fnemeet2  25465  fnejoin2  25467  neifg  25469  tailfb  25475  filnetlem3  25478  prdsbnd2  25667  heibor1lem  25681  bfp  25696  divrngidl  25801  rencldnfilem  26051  kelac1  26309  lnmlmic  26334  gicabl  26411  lmiclbs  26455  lmisfree  26460  symggen  26559  psgnunilem3  26567  stoweidlem35  26932  eldmrexrnb  27247  nbusgra  27377  onfrALT  27808  onfrALTVD  28178  bnj521  28276  bnj1189  28550  bnj1279  28559  atex  29413  llnn0  29523  lplnn0N  29554  lvoln0N  29598  pmapglb2N  29778  pmapglb2xN  29779  elpaddn0  29807  osumcllem8N  29970  pexmidlem5N  29981  diaglbN  31063  diaintclN  31066  dibglbN  31174  dibintclN  31175  dihglblem2aN  31301  dihglblem5  31306  dihglbcpreN  31308  dihintcl  31352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-v 2824  df-dif 3189  df-nul 3490
  Copyright terms: Public domain W3C validator