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

Theorem n0 3629
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 2571 . 2  |-  F/_ x A
21n0f 3628 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550    e. wcel 1725    =/= wne 2598   (/)c0 3620
This theorem is referenced by:  neq0  3630  reximdva0  3631  n0moeu  3632  pssnel  3685  r19.2z  3709  r19.2zb  3710  r19.3rz  3711  r19.3rzv  3713  uniintsn  4079  iunn0  4143  trint0  4311  intex  4348  notzfaus  4366  nnullss  4417  exss  4418  opabn0  4477  wefrc  4568  wereu2  4571  onfr  4612  reusv2lem1  4716  reusv5OLD  4725  limuni3  4824  dmxp  5080  xpnz  5284  soex  5311  dmsnn0  5327  unixp0  5395  xpco  5406  eldmrexrnb  5869  isofrlem  6052  f1oweALT  6066  fo1stres  6362  fo2ndres  6363  ecdmn0  6939  map0g  7045  ixpn0  7086  resixpfo  7092  domdifsn  7183  xpdom3  7198  fodomr  7250  mapdom3  7271  findcard2  7340  unblem2  7352  marypha1lem  7430  brwdom2  7533  unxpwdom2  7548  ixpiunwdom  7551  zfreg  7555  zfreg2  7556  epfrs  7659  scott0  7802  cplem1  7805  fseqen  7900  finacn  7923  iunfictbso  7987  aceq2  7992  dfac3  7994  dfac9  8008  kmlem6  8027  kmlem8  8029  infpss  8089  fin23lem7  8188  enfin2i  8193  fin23lem21  8211  fin23lem31  8215  isf32lem9  8233  isf34lem4  8249  axdc2lem  8320  axdc3lem4  8325  ac6c4  8353  ac9  8355  ac6s4  8362  ac9s  8365  ttukeyg  8389  fpwwe2lem12  8508  wun0  8585  tsk0  8630  gruina  8685  genpn0  8872  prlem934  8902  ltaddpr  8903  ltexprlem1  8905  prlem936  8916  reclem2pr  8917  suplem1pr  8921  supsr  8979  axpre-sup  9036  infm3  9959  supmul1  9965  supmullem2  9967  supmul  9968  infmrcl  9979  negn0  10554  zsupss  10557  xrsupsslem  10877  xrinfmsslem  10878  supxrre  10898  infmxrre  10906  ixxub  10929  ixxlb  10930  ioorebas  10998  fzn0  11062  fzon0  11148  hashgt0elexb  11663  swrdcl  11758  maxprmfct  13105  4sqlem12  13316  vdwmc  13338  ramz  13385  ramub1  13388  mreiincl  13813  mremre  13821  mreexexlem4d  13864  iscatd2  13898  drsdirfi  14387  issubg2  14951  subgint  14956  giclcl  15051  gicrcl  15052  gicsym  15053  gictr  15054  gicen  15056  gicsubgen  15057  cntzssv  15119  sylow1lem4  15227  odcau  15230  sylow3  15259  cyggex2  15498  giccyg  15501  pgpfac1lem5  15629  subrgint  15882  lss0cl  16015  lmiclcl  16134  lmicrcl  16135  lmicsym  16136  lspsnat  16209  lspprat  16217  abvn0b  16354  cnsubrg  16751  cygzn  16843  toponmre  17149  iunconlem  17482  iuncon  17483  uncon  17484  clscon  17485  2ndcdisj  17511  2ndcsep  17514  1stcelcls  17516  txcls  17628  hmphsym  17806  hmphtr  17807  hmphen  17809  haushmphlem  17811  cmphmph  17812  conhmph  17813  reghmph  17817  nrmhmph  17818  hmphdis  17820  hmphen2  17823  fbdmn0  17858  isfbas2  17859  fbssint  17862  trfbas2  17867  filtop  17879  isfil2  17880  elfg  17895  fgcl  17902  filssufilg  17935  uffix2  17948  ufildom1  17950  hauspwpwf1  18011  hausflf2  18022  alexsubALTlem2  18071  ptcmplem2  18076  cnextf  18089  tgptsmscld  18172  ustfilxp  18234  xbln0  18436  lpbl  18525  met2ndci  18544  metustfbasOLD  18587  metustfbas  18588  restmetu  18609  reconn  18851  opnreen  18854  metdsre  18875  phtpcer  19012  phtpc01  19013  phtpcco2  19016  pcohtpy  19037  cfilfcls  19219  cmetcaulem  19233  cmetcau  19234  cmetss  19259  bcthlem5  19273  ovolicc2lem2  19406  ovolicc2lem5  19409  ioorcl2  19456  ioorinv2  19459  itg11  19575  dvlip  19869  dvne0  19887  mpfrcl  19931  fta1g  20082  plyssc  20111  fta1  20217  vieta1lem2  20220  umgraex  21350  eupath  21695  isgrp2d  21815  ubthlem1  22364  shintcli  22823  fmcncfil  24309  insiga  24512  pconcon  24910  txscon  24920  cvmsss2  24953  cvmopnlem  24957  cvmfolem  24958  cvmliftmolem2  24961  cvmlift2lem10  24991  cvmliftpht  24997  cvmlift3lem8  25005  dedekind  25179  dedekindle  25180  eldm3  25377  fundmpss  25382  elima4  25396  frmin  25509  nocvxmin  25638  axcontlem4  25898  axcontlem10  25904  supaddc  26228  supadd  26229  itg2addnclem2  26247  locfincmp  26375  comppfsc  26378  neibastop1  26379  neibastop2lem  26380  neibastop2  26381  fnemeet2  26387  fnejoin2  26389  neifg  26391  tailfb  26397  filnetlem3  26400  prdsbnd2  26495  heibor1lem  26509  bfp  26524  divrngidl  26629  rencldnfilem  26872  kelac1  27129  lnmlmic  27154  gicabl  27231  lmiclbs  27275  lmisfree  27280  symggen  27379  psgnunilem3  27387  stoweidlem35  27751  2spontn0vne  28307  frgrawopreglem2  28371  onfrALT  28572  onfrALTVD  28940  iunconlem2  28984  bnj521  29041  bnj1189  29315  bnj1279  29324  atex  30140  llnn0  30250  lplnn0N  30281  lvoln0N  30325  pmapglb2N  30505  pmapglb2xN  30506  elpaddn0  30534  osumcllem8N  30697  pexmidlem5N  30708  diaglbN  31790  diaintclN  31793  dibglbN  31901  dibintclN  31902  dihglblem2aN  32028  dihglblem5  32033  dihglbcpreN  32035  dihintcl  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator