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

Theorem n0 3371
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 2385 . 2  |-  F/_ x A
21n0f 3370 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    e. wcel 1621    =/= wne 2412   (/)c0 3362
This theorem is referenced by:  neq0  3372  reximdva0  3373  n0moeu  3374  pssnel  3425  r19.2z  3449  r19.2zb  3450  r19.3rz  3451  r19.3rzv  3453  uniintsn  3797  iunn0  3860  trint0  4027  intex  4065  notzfaus  4079  nnullss  4128  exss  4129  opabn0  4188  wefrc  4280  wereu2  4283  onfr  4324  reusv2lem1  4426  reusv5OLD  4435  limuni3  4534  dmxp  4804  xpnz  5006  soex  5029  dmsnn0  5044  unixp0  5112  isofrlem  5689  f1oweALT  5703  fo1stres  5995  fo2ndres  5996  ecdmn0  6588  map0g  6693  ixpn0  6734  resixpfo  6740  domdifsn  6830  xpdom3  6845  fodomr  6897  mapdom3  6918  findcard2  6983  unblem2  6995  marypha1lem  7070  brwdom2  7171  unxpwdom2  7186  ixpiunwdom  7189  zfreg  7193  zfreg2  7194  epfrs  7297  scott0  7440  cplem1  7443  fseqen  7538  finacn  7561  iunfictbso  7625  aceq2  7630  dfac3  7632  dfac9  7646  kmlem6  7665  kmlem8  7667  infpss  7727  fin23lem7  7826  enfin2i  7831  fin23lem21  7849  fin23lem31  7853  isf32lem9  7871  isf34lem4  7887  axdc2lem  7958  axdc3lem4  7963  ac6c4  7992  ac9  7994  ac6s4  8001  ac9s  8004  ttukeyg  8028  fpwwe2lem12  8143  wun0  8220  tsk0  8265  gruina  8320  genpn0  8507  prlem934  8537  ltaddpr  8538  ltexprlem1  8540  prlem936  8551  reclem2pr  8552  suplem1pr  8556  supsr  8614  axpre-sup  8671  infm3  9593  supmul1  9599  supmullem2  9601  supmul  9602  infmrcl  9613  negn0  10183  zsupss  10186  xrsupsslem  10503  xrinfmsslem  10504  supxrre  10524  infmxrre  10532  ixxub  10555  ixxlb  10556  ioorebas  10623  fzn0  10687  fzon0  10769  swrdcl  11329  maxprmfct  12666  4sqlem12  12877  vdwmc  12899  ramz  12946  ramub1  12949  mreiincl  13370  mremre  13378  iscatd2  13427  drsdirfi  13916  issubg2  14471  subgint  14476  giclcl  14571  gicrcl  14572  gicsym  14573  gictr  14574  gicen  14576  gicsubgen  14577  cntzssv  14639  sylow1lem4  14747  odcau  14750  sylow3  14779  cyggex2  15018  giccyg  15021  pgpfac1lem5  15149  subrgint  15402  lss0cl  15539  lmiclcl  15658  lmicrcl  15659  lmicsym  15660  lspsnat  15732  lspprat  15740  abvn0b  15875  cnsubrg  16264  cygzn  16356  toponmre  16662  iunconlem  16985  iuncon  16986  uncon  16987  clscon  16988  2ndcdisj  17014  2ndcsep  17017  1stcelcls  17019  txcls  17131  hmphsym  17305  hmphtr  17306  hmphen  17308  haushmphlem  17310  cmphmph  17311  conhmph  17312  reghmph  17316  nrmhmph  17317  hmphdis  17319  hmphen2  17322  fbdmn0  17361  isfbas2  17362  fbssint  17365  trfbas2  17370  filtop  17382  isfil2  17383  elfg  17398  fgcl  17405  filssufilg  17438  uffix2  17451  ufildom1  17453  hauspwpwf1  17514  hausflf2  17525  alexsubALTlem2  17574  ptcmplem2  17579  tgptsmscld  17665  xbln0  17797  lpbl  17881  met2ndci  17900  reconn  18165  opnreen  18168  metdsre  18189  phtpcer  18325  phtpc01  18326  phtpcco2  18329  pcohtpy  18350  cfilfcls  18532  cmetcaulem  18546  cmetcau  18547  cmetss  18572  bcthlem5  18582  ovolicc2lem2  18709  ovolicc2lem5  18712  ioorcl2  18759  ioorinv2  18762  itg11  18878  dvlip  19172  dvne0  19190  mpfrcl  19234  fta1g  19385  plyssc  19414  fta1  19520  vieta1lem2  19523  isgrp2d  20732  ubthlem1  21279  shintcli  21738  pconcon  22933  txscon  22943  cvmsss2  22976  cvmopnlem  22980  cvmfolem  22981  cvmliftmolem2  22984  cvmlift2lem10  23014  cvmliftpht  23020  cvmlift3lem8  23028  umgraex  23046  eupath  23076  dedekind  23252  dedekindle  23253  fundmpss  23290  frmin  23410  nocvxmin  23513  axfelem15  23528  axcontlem4  23769  axcontlem10  23775  prl  24333  dstr  24337  aline  25240  isconcl6a  25269  isconcl6ab  25270  lppotos  25310  bhp3  25343  locfincmp  25470  comppfsc  25473  neibastop1  25474  neibastop2lem  25475  neibastop2  25476  fnemeet2  25482  fnejoin2  25484  neifg  25486  tailfb  25492  filnetlem3  25495  prdsbnd2  25685  heibor1lem  25699  bfp  25714  divrngidl  25819  rencldnfilem  26069  kelac1  26327  lnmlmic  26352  gicabl  26429  lmiclbs  26473  lmisfree  26478  symggen  26577  psgnunilem3  26585  onfrALT  27007  onfrALTVD  27357  bnj521  27454  bnj1189  27728  bnj1279  27737  atex  28284  llnn0  28394  lplnn0N  28425  lvoln0N  28469  pmapglb2N  28649  pmapglb2xN  28650  elpaddn0  28678  osumcllem8N  28841  pexmidlem5N  28852  diaglbN  29934  diaintclN  29937  dibglbN  30045  dibintclN  30046  dihglblem2aN  30172  dihglblem5  30177  dihglbcpreN  30179  dihintcl  30223
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-nul 3363
  Copyright terms: Public domain W3C validator