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

Theorem n0 3605
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 2548 . 2  |-  F/_ x A
21n0f 3604 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1547    e. wcel 1721    =/= wne 2575   (/)c0 3596
This theorem is referenced by:  neq0  3606  reximdva0  3607  n0moeu  3608  pssnel  3661  r19.2z  3685  r19.2zb  3686  r19.3rz  3687  r19.3rzv  3689  uniintsn  4055  iunn0  4119  trint0  4287  intex  4324  notzfaus  4342  nnullss  4393  exss  4394  opabn0  4453  wefrc  4544  wereu2  4547  onfr  4588  reusv2lem1  4691  reusv5OLD  4700  limuni3  4799  dmxp  5055  xpnz  5259  soex  5286  dmsnn0  5302  unixp0  5370  xpco  5381  eldmrexrnb  5844  isofrlem  6027  f1oweALT  6041  fo1stres  6337  fo2ndres  6338  ecdmn0  6914  map0g  7020  ixpn0  7061  resixpfo  7067  domdifsn  7158  xpdom3  7173  fodomr  7225  mapdom3  7246  findcard2  7315  unblem2  7327  marypha1lem  7404  brwdom2  7505  unxpwdom2  7520  ixpiunwdom  7523  zfreg  7527  zfreg2  7528  epfrs  7631  scott0  7774  cplem1  7777  fseqen  7872  finacn  7895  iunfictbso  7959  aceq2  7964  dfac3  7966  dfac9  7980  kmlem6  7999  kmlem8  8001  infpss  8061  fin23lem7  8160  enfin2i  8165  fin23lem21  8183  fin23lem31  8187  isf32lem9  8205  isf34lem4  8221  axdc2lem  8292  axdc3lem4  8297  ac6c4  8325  ac9  8327  ac6s4  8334  ac9s  8337  ttukeyg  8361  fpwwe2lem12  8480  wun0  8557  tsk0  8602  gruina  8657  genpn0  8844  prlem934  8874  ltaddpr  8875  ltexprlem1  8877  prlem936  8888  reclem2pr  8889  suplem1pr  8893  supsr  8951  axpre-sup  9008  infm3  9931  supmul1  9937  supmullem2  9939  supmul  9940  infmrcl  9951  negn0  10526  zsupss  10529  xrsupsslem  10849  xrinfmsslem  10850  supxrre  10870  infmxrre  10878  ixxub  10901  ixxlb  10902  ioorebas  10970  fzn0  11034  fzon0  11119  hashgt0elexb  11634  swrdcl  11729  maxprmfct  13076  4sqlem12  13287  vdwmc  13309  ramz  13356  ramub1  13359  mreiincl  13784  mremre  13792  mreexexlem4d  13835  iscatd2  13869  drsdirfi  14358  issubg2  14922  subgint  14927  giclcl  15022  gicrcl  15023  gicsym  15024  gictr  15025  gicen  15027  gicsubgen  15028  cntzssv  15090  sylow1lem4  15198  odcau  15201  sylow3  15230  cyggex2  15469  giccyg  15472  pgpfac1lem5  15600  subrgint  15853  lss0cl  15986  lmiclcl  16105  lmicrcl  16106  lmicsym  16107  lspsnat  16180  lspprat  16188  abvn0b  16325  cnsubrg  16722  cygzn  16814  toponmre  17120  iunconlem  17451  iuncon  17452  uncon  17453  clscon  17454  2ndcdisj  17480  2ndcsep  17483  1stcelcls  17485  txcls  17597  hmphsym  17775  hmphtr  17776  hmphen  17778  haushmphlem  17780  cmphmph  17781  conhmph  17782  reghmph  17786  nrmhmph  17787  hmphdis  17789  hmphen2  17792  fbdmn0  17827  isfbas2  17828  fbssint  17831  trfbas2  17836  filtop  17848  isfil2  17849  elfg  17864  fgcl  17871  filssufilg  17904  uffix2  17917  ufildom1  17919  hauspwpwf1  17980  hausflf2  17991  alexsubALTlem2  18040  ptcmplem2  18045  cnextf  18058  tgptsmscld  18141  ustfilxp  18203  xbln0  18405  lpbl  18494  met2ndci  18513  metustfbasOLD  18556  metustfbas  18557  restmetu  18578  reconn  18820  opnreen  18823  metdsre  18844  phtpcer  18981  phtpc01  18982  phtpcco2  18985  pcohtpy  19006  cfilfcls  19188  cmetcaulem  19202  cmetcau  19203  cmetss  19228  bcthlem5  19242  ovolicc2lem2  19375  ovolicc2lem5  19378  ioorcl2  19425  ioorinv2  19428  itg11  19544  dvlip  19838  dvne0  19856  mpfrcl  19900  fta1g  20051  plyssc  20080  fta1  20186  vieta1lem2  20189  umgraex  21319  eupath  21664  isgrp2d  21784  ubthlem1  22333  shintcli  22792  fmcncfil  24278  insiga  24481  pconcon  24879  txscon  24889  cvmsss2  24922  cvmopnlem  24926  cvmfolem  24927  cvmliftmolem2  24930  cvmlift2lem10  24960  cvmliftpht  24966  cvmlift3lem8  24974  dedekind  25148  dedekindle  25149  eldm3  25341  fundmpss  25344  frmin  25464  nocvxmin  25567  axcontlem4  25818  axcontlem10  25824  supaddc  26145  supadd  26146  itg2addnclem2  26164  locfincmp  26282  comppfsc  26285  neibastop1  26286  neibastop2lem  26287  neibastop2  26288  fnemeet2  26294  fnejoin2  26296  neifg  26298  tailfb  26304  filnetlem3  26307  prdsbnd2  26402  heibor1lem  26416  bfp  26431  divrngidl  26536  rencldnfilem  26779  kelac1  27037  lnmlmic  27062  gicabl  27139  lmiclbs  27183  lmisfree  27188  symggen  27287  psgnunilem3  27295  stoweidlem35  27659  2spontn0vne  28092  frgrawopreglem2  28156  onfrALT  28354  onfrALTVD  28721  iunconlem2  28766  bnj521  28822  bnj1189  29096  bnj1279  29105  atex  29900  llnn0  30010  lplnn0N  30041  lvoln0N  30085  pmapglb2N  30265  pmapglb2xN  30266  elpaddn0  30294  osumcllem8N  30457  pexmidlem5N  30468  diaglbN  31550  diaintclN  31553  dibglbN  31661  dibintclN  31662  dihglblem2aN  31788  dihglblem5  31793  dihglbcpreN  31795  dihintcl  31839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-v 2926  df-dif 3291  df-nul 3597
  Copyright terms: Public domain W3C validator