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

Theorem n0 3794
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
Distinct variable group:   ,

Proof of Theorem n0
StepHypRef Expression
1 nfcv 2619 . 2
21n0f 3793 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612  e.wcel 1818  =/=wne 2652   c0 3784
This theorem is referenced by:  neq0  3795  reximdva0  3796  rspn0  3797  n0moeu  3798  pssnel  3893  r19.2z  3918  r19.2zb  3919  r19.3rz  3920  r19.3rzv  3922  uniintsn  4324  iunn0  4390  trint0  4562  intex  4608  notzfaus  4627  reusv2lem1  4653  reusv5OLD  4662  nnullss  4714  exss  4715  opabn0  4783  wefrc  4878  wereu2  4881  onfr  4922  dmxp  5226  xpnz  5431  dmsnn0  5478  unixp0  5546  xpco  5552  fveqdmss  6026  eldmrexrnb  6038  isofrlem  6236  limuni3  6687  soex  6743  f1oweALT  6784  fo1stres  6824  fo2ndres  6825  ecdmn0  7373  map0g  7478  ixpn0  7521  resixpfo  7527  domdifsn  7620  xpdom3  7635  fodomr  7688  mapdom3  7709  findcard2  7780  unblem2  7793  marypha1lem  7913  brwdom2  8020  unxpwdom2  8035  ixpiunwdom  8038  zfreg  8042  zfreg2  8043  epfrs  8183  scott0  8325  cplem1  8328  fseqen  8429  finacn  8452  iunfictbso  8516  aceq2  8521  dfac3  8523  dfac9  8537  kmlem6  8556  kmlem8  8558  infpss  8618  fin23lem7  8717  enfin2i  8722  fin23lem21  8740  fin23lem31  8744  isf32lem9  8762  isf34lem4  8778  axdc2lem  8849  axdc3lem4  8854  ac6c4  8882  ac9  8884  ac6s4  8891  ac9s  8894  ttukeyg  8918  fpwwe2lem12  9040  wun0  9117  tsk0  9162  gruina  9217  genpn0  9402  prlem934  9432  ltaddpr  9433  ltexprlem1  9435  prlem936  9446  reclem2pr  9447  suplem1pr  9451  supsr  9510  axpre-sup  9567  dedekind  9765  dedekindle  9766  infm3  10527  supmul1  10533  supmullem2  10535  supmul  10536  infmrcl  10547  negn0  11197  zsupss  11200  xrsupsslem  11527  xrinfmsslem  11528  supxrre  11548  infmxrre  11556  ixxub  11579  ixxlb  11580  ioorebas  11655  fzn0  11729  fzon0  11845  hashgt0elexb  12467  swrdcl  12646  maxprmfct  14254  4sqlem12  14474  vdwmc  14496  ramz  14543  ramub1  14546  mreiincl  14993  mremre  15001  mreexexlem4d  15044  iscatd2  15078  drsdirfi  15567  opifismgm  15885  issubg2  16216  subgint  16225  giclcl  16320  gicrcl  16321  gicsym  16322  gictr  16323  gicen  16325  gicsubgen  16326  cntzssv  16366  symggen  16495  psgnunilem3  16521  sylow1lem4  16621  odcau  16624  sylow3  16653  cyggex2  16899  giccyg  16902  pgpfac1lem5  17130  brric2  17394  subrgint  17451  lss0cl  17593  lmiclcl  17716  lmicrcl  17717  lmicsym  17718  lspsnat  17791  lspprat  17799  abvn0b  17951  mpfrcl  18187  ply1frcl  18355  cnsubrg  18478  cygzn  18609  lmiclbs  18872  lmisfree  18877  lmictra  18880  mdetdiaglem  19100  mdet0  19108  toponmre  19594  iunconlem  19928  iuncon  19929  uncon  19930  clscon  19931  2ndcdisj  19957  2ndcsep  19960  1stcelcls  19962  locfincmp  20027  comppfsc  20033  txcls  20105  hmphsym  20283  hmphtr  20284  hmphen  20286  haushmphlem  20288  cmphmph  20289  conhmph  20290  reghmph  20294  nrmhmph  20295  hmphdis  20297  hmphen2  20300  fbdmn0  20335  isfbas2  20336  fbssint  20339  trfbas2  20344  filtop  20356  isfil2  20357  elfg  20372  fgcl  20379  filssufilg  20412  uffix2  20425  ufildom1  20427  hauspwpwf1  20488  hausflf2  20499  alexsubALTlem2  20548  ptcmplem2  20553  cnextf  20566  tgptsmscld  20653  ustfilxp  20715  xbln0  20917  lpbl  21006  met2ndci  21025  metustfbasOLD  21068  metustfbas  21069  restmetu  21090  reconn  21333  opnreen  21336  metdsre  21357  phtpcer  21495  phtpc01  21496  phtpcco2  21499  pcohtpy  21520  cfilfcls  21713  cmetcaulem  21727  cmetcau  21728  cmetss  21753  bcthlem5  21767  ovolicc2lem2  21929  ovolicc2lem5  21932  ioorcl2  21981  ioorinv2  21984  itg11  22098  dvlip  22394  dvne0  22412  fta1g  22568  plyssc  22597  fta1  22704  vieta1lem2  22707  hpgerlem  24134  axcontlem4  24270  axcontlem10  24276  umgraex  24323  2spontn0vne  24887  eupath  24981  usgn0fidegnn0  25029  frgrawopreglem2  25045  isgrp2d  25237  ubthlem1  25786  shintcli  26247  fpwrelmapffslem  27555  fmcncfil  27913  insiga  28137  pconcon  28676  txscon  28686  cvmsss2  28719  cvmopnlem  28723  cvmfolem  28724  cvmliftmolem2  28727  cvmlift2lem10  28757  cvmliftpht  28763  cvmlift3lem8  28771  eldm3  29191  fundmpss  29196  elima4  29209  frmin  29322  nocvxmin  29451  supaddc  30041  supadd  30042  itg2addnclem2  30067  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  fnemeet2  30185  fnejoin2  30187  neifg  30189  tailfb  30195  filnetlem3  30198  prdsbnd2  30291  heibor1lem  30305  bfp  30320  divrngidl  30425  rencldnfilem  30754  kelac1  31009  lnmlmic  31034  gicabl  31047  suprnmpt  31451  fsumnncl  31572  ellimciota  31620  islpcn  31645  lptre2pt  31646  stoweidlem35  31817  fourierdlem31  31920  fourier2  32010  mgmpropd  32463  opmpt2ismgm  32495  cic  32583  nzerooringczr  32880  alscn0d  33210  onfrALT  33321  onfrALTVD  33691  iunconlem2  33735  bnj521  33792  bnj1189  34065  bnj1279  34074  bj-n0i  34503  atex  35130  llnn0  35240  lplnn0N  35271  lvoln0N  35315  pmapglb2N  35495  pmapglb2xN  35496  elpaddn0  35524  osumcllem8N  35687  pexmidlem5N  35698  diaglbN  36782  diaintclN  36785  dibglbN  36893  dibintclN  36894  dihglblem2aN  37020  dihglblem5  37025  dihglbcpreN  37027  dihintcl  37071  xpcogend  37773  ndisj  37793
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-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator