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

Theorem n0 3406
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 2392 . 2  |-  F/_ x A
21n0f 3405 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    e. wcel 1621    =/= wne 2419   (/)c0 3397
This theorem is referenced by:  neq0  3407  reximdva0  3408  n0moeu  3409  pssnel  3461  r19.2z  3485  r19.2zb  3486  r19.3rz  3487  r19.3rzv  3489  uniintsn  3840  iunn0  3903  trint0  4070  intex  4109  notzfaus  4123  nnullss  4172  exss  4173  opabn0  4232  wefrc  4324  wereu2  4327  onfr  4368  reusv2lem1  4472  reusv5OLD  4481  limuni3  4580  dmxp  4850  xpnz  5052  soex  5075  dmsnn0  5090  unixp0  5158  isofrlem  5736  f1oweALT  5750  fo1stres  6042  fo2ndres  6043  ecdmn0  6635  map0g  6740  ixpn0  6781  resixpfo  6787  domdifsn  6878  xpdom3  6893  fodomr  6945  mapdom3  6966  findcard2  7031  unblem2  7043  marypha1lem  7119  brwdom2  7220  unxpwdom2  7235  ixpiunwdom  7238  zfreg  7242  zfreg2  7243  epfrs  7346  scott0  7489  cplem1  7492  fseqen  7587  finacn  7610  iunfictbso  7674  aceq2  7679  dfac3  7681  dfac9  7695  kmlem6  7714  kmlem8  7716  infpss  7776  fin23lem7  7875  enfin2i  7880  fin23lem21  7898  fin23lem31  7902  isf32lem9  7920  isf34lem4  7936  axdc2lem  8007  axdc3lem4  8012  ac6c4  8041  ac9  8043  ac6s4  8050  ac9s  8053  ttukeyg  8077  fpwwe2lem12  8196  wun0  8273  tsk0  8318  gruina  8373  genpn0  8560  prlem934  8590  ltaddpr  8591  ltexprlem1  8593  prlem936  8604  reclem2pr  8605  suplem1pr  8609  supsr  8667  axpre-sup  8724  infm3  9646  supmul1  9652  supmullem2  9654  supmul  9655  infmrcl  9666  negn0  10236  zsupss  10239  xrsupsslem  10556  xrinfmsslem  10557  supxrre  10577  infmxrre  10585  ixxub  10608  ixxlb  10609  ioorebas  10676  fzn0  10740  fzon0  10822  swrdcl  11382  maxprmfct  12719  4sqlem12  12930  vdwmc  12952  ramz  12999  ramub1  13002  mreiincl  13425  mremre  13433  mreexexlem4d  13476  iscatd2  13510  drsdirfi  13999  issubg2  14563  subgint  14568  giclcl  14663  gicrcl  14664  gicsym  14665  gictr  14666  gicen  14668  gicsubgen  14669  cntzssv  14731  sylow1lem4  14839  odcau  14842  sylow3  14871  cyggex2  15110  giccyg  15113  pgpfac1lem5  15241  subrgint  15494  lss0cl  15631  lmiclcl  15750  lmicrcl  15751  lmicsym  15752  lspsnat  15825  lspprat  15833  abvn0b  15970  cnsubrg  16359  cygzn  16451  toponmre  16757  iunconlem  17080  iuncon  17081  uncon  17082  clscon  17083  2ndcdisj  17109  2ndcsep  17112  1stcelcls  17114  txcls  17226  hmphsym  17400  hmphtr  17401  hmphen  17403  haushmphlem  17405  cmphmph  17406  conhmph  17407  reghmph  17411  nrmhmph  17412  hmphdis  17414  hmphen2  17417  fbdmn0  17456  isfbas2  17457  fbssint  17460  trfbas2  17465  filtop  17477  isfil2  17478  elfg  17493  fgcl  17500  filssufilg  17533  uffix2  17546  ufildom1  17548  hauspwpwf1  17609  hausflf2  17620  alexsubALTlem2  17669  ptcmplem2  17674  tgptsmscld  17760  xbln0  17892  lpbl  17976  met2ndci  17995  reconn  18260  opnreen  18263  metdsre  18284  phtpcer  18420  phtpc01  18421  phtpcco2  18424  pcohtpy  18445  cfilfcls  18627  cmetcaulem  18641  cmetcau  18642  cmetss  18667  bcthlem5  18677  ovolicc2lem2  18804  ovolicc2lem5  18807  ioorcl2  18854  ioorinv2  18857  itg11  18973  dvlip  19267  dvne0  19285  mpfrcl  19329  fta1g  19480  plyssc  19509  fta1  19615  vieta1lem2  19618  isgrp2d  20827  ubthlem1  21374  shintcli  21833  pconcon  23099  txscon  23109  cvmsss2  23142  cvmopnlem  23146  cvmfolem  23147  cvmliftmolem2  23150  cvmlift2lem10  23180  cvmliftpht  23186  cvmlift3lem8  23194  umgraex  23212  eupath  23242  dedekind  23418  dedekindle  23419  fundmpss  23456  frmin  23576  nocvxmin  23679  axfelem15  23694  axcontlem4  23935  axcontlem10  23941  prl  24499  dstr  24503  aline  25406  isconcl6a  25435  isconcl6ab  25436  lppotos  25476  bhp3  25509  locfincmp  25636  comppfsc  25639  neibastop1  25640  neibastop2lem  25641  neibastop2  25642  fnemeet2  25648  fnejoin2  25650  neifg  25652  tailfb  25658  filnetlem3  25661  prdsbnd2  25851  heibor1lem  25865  bfp  25880  divrngidl  25985  rencldnfilem  26235  kelac1  26493  lnmlmic  26518  gicabl  26595  lmiclbs  26639  lmisfree  26644  symggen  26743  psgnunilem3  26751  stoweidlem35  27084  onfrALT  27330  onfrALTVD  27680  bnj521  27777  bnj1189  28051  bnj1279  28060  atex  28725  llnn0  28835  lplnn0N  28866  lvoln0N  28910  pmapglb2N  29090  pmapglb2xN  29091  elpaddn0  29119  osumcllem8N  29282  pexmidlem5N  29293  diaglbN  30375  diaintclN  30378  dibglbN  30486  dibintclN  30487  dihglblem2aN  30613  dihglblem5  30618  dihglbcpreN  30620  dihintcl  30664
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-nul 3398
  Copyright terms: Public domain W3C validator