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

Theorem n0 3439
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 2394 . 2  |-  F/_ x A
21n0f 3438 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    e. wcel 1621    =/= wne 2421   (/)c0 3430
This theorem is referenced by:  neq0  3440  reximdva0  3441  n0moeu  3442  pssnel  3494  r19.2z  3518  r19.2zb  3519  r19.3rz  3520  r19.3rzv  3522  uniintsn  3873  iunn0  3936  trint0  4104  intex  4143  notzfaus  4157  nnullss  4207  exss  4208  opabn0  4267  wefrc  4359  wereu2  4362  onfr  4403  reusv2lem1  4507  reusv5OLD  4516  limuni3  4615  dmxp  4885  xpnz  5087  soex  5110  dmsnn0  5125  unixp0  5193  isofrlem  5771  f1oweALT  5785  fo1stres  6077  fo2ndres  6078  ecdmn0  6670  map0g  6775  ixpn0  6816  resixpfo  6822  domdifsn  6913  xpdom3  6928  fodomr  6980  mapdom3  7001  findcard2  7066  unblem2  7078  marypha1lem  7154  brwdom2  7255  unxpwdom2  7270  ixpiunwdom  7273  zfreg  7277  zfreg2  7278  epfrs  7381  scott0  7524  cplem1  7527  fseqen  7622  finacn  7645  iunfictbso  7709  aceq2  7714  dfac3  7716  dfac9  7730  kmlem6  7749  kmlem8  7751  infpss  7811  fin23lem7  7910  enfin2i  7915  fin23lem21  7933  fin23lem31  7937  isf32lem9  7955  isf34lem4  7971  axdc2lem  8042  axdc3lem4  8047  ac6c4  8076  ac9  8078  ac6s4  8085  ac9s  8088  ttukeyg  8112  fpwwe2lem12  8231  wun0  8308  tsk0  8353  gruina  8408  genpn0  8595  prlem934  8625  ltaddpr  8626  ltexprlem1  8628  prlem936  8639  reclem2pr  8640  suplem1pr  8644  supsr  8702  axpre-sup  8759  infm3  9681  supmul1  9687  supmullem2  9689  supmul  9690  infmrcl  9701  negn0  10271  zsupss  10274  xrsupsslem  10591  xrinfmsslem  10592  supxrre  10612  infmxrre  10620  ixxub  10643  ixxlb  10644  ioorebas  10711  fzn0  10775  fzon0  10857  swrdcl  11417  maxprmfct  12754  4sqlem12  12965  vdwmc  12987  ramz  13034  ramub1  13037  mreiincl  13460  mremre  13468  mreexexlem4d  13511  iscatd2  13545  drsdirfi  14034  issubg2  14598  subgint  14603  giclcl  14698  gicrcl  14699  gicsym  14700  gictr  14701  gicen  14703  gicsubgen  14704  cntzssv  14766  sylow1lem4  14874  odcau  14877  sylow3  14906  cyggex2  15145  giccyg  15148  pgpfac1lem5  15276  subrgint  15529  lss0cl  15666  lmiclcl  15785  lmicrcl  15786  lmicsym  15787  lspsnat  15860  lspprat  15868  abvn0b  16005  cnsubrg  16394  cygzn  16486  toponmre  16792  iunconlem  17115  iuncon  17116  uncon  17117  clscon  17118  2ndcdisj  17144  2ndcsep  17147  1stcelcls  17149  txcls  17261  hmphsym  17435  hmphtr  17436  hmphen  17438  haushmphlem  17440  cmphmph  17441  conhmph  17442  reghmph  17446  nrmhmph  17447  hmphdis  17449  hmphen2  17452  fbdmn0  17491  isfbas2  17492  fbssint  17495  trfbas2  17500  filtop  17512  isfil2  17513  elfg  17528  fgcl  17535  filssufilg  17568  uffix2  17581  ufildom1  17583  hauspwpwf1  17644  hausflf2  17655  alexsubALTlem2  17704  ptcmplem2  17709  tgptsmscld  17795  xbln0  17927  lpbl  18011  met2ndci  18030  reconn  18295  opnreen  18298  metdsre  18319  phtpcer  18455  phtpc01  18456  phtpcco2  18459  pcohtpy  18480  cfilfcls  18662  cmetcaulem  18676  cmetcau  18677  cmetss  18702  bcthlem5  18712  ovolicc2lem2  18839  ovolicc2lem5  18842  ioorcl2  18889  ioorinv2  18892  itg11  19008  dvlip  19302  dvne0  19320  mpfrcl  19364  fta1g  19515  plyssc  19544  fta1  19650  vieta1lem2  19653  isgrp2d  20862  ubthlem1  21409  shintcli  21868  pconcon  23134  txscon  23144  cvmsss2  23177  cvmopnlem  23181  cvmfolem  23182  cvmliftmolem2  23185  cvmlift2lem10  23215  cvmliftpht  23221  cvmlift3lem8  23229  umgraex  23247  eupath  23277  dedekind  23453  dedekindle  23454  fundmpss  23491  frmin  23611  nocvxmin  23714  axfelem15  23729  axcontlem4  23970  axcontlem10  23976  prl  24534  dstr  24538  aline  25441  isconcl6a  25470  isconcl6ab  25471  lppotos  25511  bhp3  25544  locfincmp  25671  comppfsc  25674  neibastop1  25675  neibastop2lem  25676  neibastop2  25677  fnemeet2  25683  fnejoin2  25685  neifg  25687  tailfb  25693  filnetlem3  25696  prdsbnd2  25886  heibor1lem  25900  bfp  25915  divrngidl  26020  rencldnfilem  26270  kelac1  26528  lnmlmic  26553  gicabl  26630  lmiclbs  26674  lmisfree  26679  symggen  26778  psgnunilem3  26786  stoweidlem35  27119  onfrALT  27367  onfrALTVD  27717  bnj521  27814  bnj1189  28088  bnj1279  28097  atex  28762  llnn0  28872  lplnn0N  28903  lvoln0N  28947  pmapglb2N  29127  pmapglb2xN  29128  elpaddn0  29156  osumcllem8N  29319  pexmidlem5N  29330  diaglbN  30412  diaintclN  30415  dibglbN  30523  dibintclN  30524  dihglblem2aN  30650  dihglblem5  30655  dihglbcpreN  30657  dihintcl  30701
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-nul 3431
  Copyright terms: Public domain W3C validator