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

Theorem n0 3465
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 2420 . 2  |-  F/_ x A
21n0f 3464 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1529    e. wcel 1685    =/= wne 2447   (/)c0 3456
This theorem is referenced by:  neq0  3466  reximdva0  3467  n0moeu  3468  pssnel  3520  r19.2z  3544  r19.2zb  3545  r19.3rz  3546  r19.3rzv  3548  uniintsn  3900  iunn0  3963  trint0  4131  intex  4170  notzfaus  4184  nnullss  4234  exss  4235  opabn0  4294  wefrc  4386  wereu2  4389  onfr  4430  reusv2lem1  4534  reusv5OLD  4543  limuni3  4642  dmxp  4896  xpnz  5098  soex  5121  dmsnn0  5136  unixp0  5204  isofrlem  5798  f1oweALT  5812  fo1stres  6104  fo2ndres  6105  ecdmn0  6697  map0g  6802  ixpn0  6843  resixpfo  6849  domdifsn  6940  xpdom3  6955  fodomr  7007  mapdom3  7028  findcard2  7093  unblem2  7105  marypha1lem  7181  brwdom2  7282  unxpwdom2  7297  ixpiunwdom  7300  zfreg  7304  zfreg2  7305  epfrs  7408  scott0  7551  cplem1  7554  fseqen  7649  finacn  7672  iunfictbso  7736  aceq2  7741  dfac3  7743  dfac9  7757  kmlem6  7776  kmlem8  7778  infpss  7838  fin23lem7  7937  enfin2i  7942  fin23lem21  7960  fin23lem31  7964  isf32lem9  7982  isf34lem4  7998  axdc2lem  8069  axdc3lem4  8074  ac6c4  8103  ac9  8105  ac6s4  8112  ac9s  8115  ttukeyg  8139  fpwwe2lem12  8258  wun0  8335  tsk0  8380  gruina  8435  genpn0  8622  prlem934  8652  ltaddpr  8653  ltexprlem1  8655  prlem936  8666  reclem2pr  8667  suplem1pr  8671  supsr  8729  axpre-sup  8786  infm3  9708  supmul1  9714  supmullem2  9716  supmul  9717  infmrcl  9728  negn0  10299  zsupss  10302  xrsupsslem  10619  xrinfmsslem  10620  supxrre  10640  infmxrre  10648  ixxub  10671  ixxlb  10672  ioorebas  10739  fzn0  10803  fzon0  10885  swrdcl  11446  maxprmfct  12786  4sqlem12  12997  vdwmc  13019  ramz  13066  ramub1  13069  mreiincl  13492  mremre  13500  mreexexlem4d  13543  iscatd2  13577  drsdirfi  14066  issubg2  14630  subgint  14635  giclcl  14730  gicrcl  14731  gicsym  14732  gictr  14733  gicen  14735  gicsubgen  14736  cntzssv  14798  sylow1lem4  14906  odcau  14909  sylow3  14938  cyggex2  15177  giccyg  15180  pgpfac1lem5  15308  subrgint  15561  lss0cl  15698  lmiclcl  15817  lmicrcl  15818  lmicsym  15819  lspsnat  15892  lspprat  15900  abvn0b  16037  cnsubrg  16426  cygzn  16518  toponmre  16824  iunconlem  17147  iuncon  17148  uncon  17149  clscon  17150  2ndcdisj  17176  2ndcsep  17179  1stcelcls  17181  txcls  17293  hmphsym  17467  hmphtr  17468  hmphen  17470  haushmphlem  17472  cmphmph  17473  conhmph  17474  reghmph  17478  nrmhmph  17479  hmphdis  17481  hmphen2  17484  fbdmn0  17523  isfbas2  17524  fbssint  17527  trfbas2  17532  filtop  17544  isfil2  17545  elfg  17560  fgcl  17567  filssufilg  17600  uffix2  17613  ufildom1  17615  hauspwpwf1  17676  hausflf2  17687  alexsubALTlem2  17736  ptcmplem2  17741  tgptsmscld  17827  xbln0  17959  lpbl  18043  met2ndci  18062  reconn  18327  opnreen  18330  metdsre  18351  phtpcer  18487  phtpc01  18488  phtpcco2  18491  pcohtpy  18512  cfilfcls  18694  cmetcaulem  18708  cmetcau  18709  cmetss  18734  bcthlem5  18744  ovolicc2lem2  18871  ovolicc2lem5  18874  ioorcl2  18921  ioorinv2  18924  itg11  19040  dvlip  19334  dvne0  19352  mpfrcl  19396  fta1g  19547  plyssc  19576  fta1  19682  vieta1lem2  19685  isgrp2d  20894  ubthlem1  21441  shintcli  21900  pconcon  23166  txscon  23176  cvmsss2  23209  cvmopnlem  23213  cvmfolem  23214  cvmliftmolem2  23217  cvmlift2lem10  23247  cvmliftpht  23253  cvmlift3lem8  23261  umgraex  23279  eupath  23309  dedekind  23485  dedekindle  23486  fundmpss  23523  frmin  23643  nocvxmin  23746  axfelem15  23761  axcontlem4  24002  axcontlem10  24008  prl  24566  dstr  24570  aline  25473  isconcl6a  25502  isconcl6ab  25503  lppotos  25543  bhp3  25576  locfincmp  25703  comppfsc  25706  neibastop1  25707  neibastop2lem  25708  neibastop2  25709  fnemeet2  25715  fnejoin2  25717  neifg  25719  tailfb  25725  filnetlem3  25728  prdsbnd2  25918  heibor1lem  25932  bfp  25947  divrngidl  26052  rencldnfilem  26302  kelac1  26560  lnmlmic  26585  gicabl  26662  lmiclbs  26706  lmisfree  26711  symggen  26810  psgnunilem3  26818  stoweidlem35  27183  onfrALT  27585  onfrALTVD  27935  bnj521  28032  bnj1189  28306  bnj1279  28315  atex  28862  llnn0  28972  lplnn0N  29003  lvoln0N  29047  pmapglb2N  29227  pmapglb2xN  29228  elpaddn0  29256  osumcllem8N  29419  pexmidlem5N  29430  diaglbN  30512  diaintclN  30515  dibglbN  30623  dibintclN  30624  dihglblem2aN  30750  dihglblem5  30755  dihglbcpreN  30757  dihintcl  30801
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator