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

Theorem n0 3464
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 2419 . 2  |-  F/_ x A
21n0f 3463 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528    e. wcel 1684    =/= wne 2446   (/)c0 3455
This theorem is referenced by:  neq0  3465  reximdva0  3466  n0moeu  3467  pssnel  3519  r19.2z  3543  r19.2zb  3544  r19.3rz  3545  r19.3rzv  3547  uniintsn  3899  iunn0  3962  trint0  4130  intex  4167  notzfaus  4185  nnullss  4235  exss  4236  opabn0  4295  wefrc  4387  wereu2  4390  onfr  4431  reusv2lem1  4535  reusv5OLD  4544  limuni3  4643  dmxp  4897  xpnz  5099  soex  5122  dmsnn0  5138  unixp0  5206  isofrlem  5837  f1oweALT  5851  fo1stres  6143  fo2ndres  6144  ecdmn0  6702  map0g  6807  ixpn0  6848  resixpfo  6854  domdifsn  6945  xpdom3  6960  fodomr  7012  mapdom3  7033  findcard2  7098  unblem2  7110  marypha1lem  7186  brwdom2  7287  unxpwdom2  7302  ixpiunwdom  7305  zfreg  7309  zfreg2  7310  epfrs  7413  scott0  7556  cplem1  7559  fseqen  7654  finacn  7677  iunfictbso  7741  aceq2  7746  dfac3  7748  dfac9  7762  kmlem6  7781  kmlem8  7783  infpss  7843  fin23lem7  7942  enfin2i  7947  fin23lem21  7965  fin23lem31  7969  isf32lem9  7987  isf34lem4  8003  axdc2lem  8074  axdc3lem4  8079  ac6c4  8108  ac9  8110  ac6s4  8117  ac9s  8120  ttukeyg  8144  fpwwe2lem12  8263  wun0  8340  tsk0  8385  gruina  8440  genpn0  8627  prlem934  8657  ltaddpr  8658  ltexprlem1  8660  prlem936  8671  reclem2pr  8672  suplem1pr  8676  supsr  8734  axpre-sup  8791  infm3  9713  supmul1  9719  supmullem2  9721  supmul  9722  infmrcl  9733  negn0  10304  zsupss  10307  xrsupsslem  10625  xrinfmsslem  10626  supxrre  10646  infmxrre  10654  ixxub  10677  ixxlb  10678  ioorebas  10745  fzn0  10809  fzon0  10891  swrdcl  11452  maxprmfct  12792  4sqlem12  13003  vdwmc  13025  ramz  13072  ramub1  13075  mreiincl  13498  mremre  13506  mreexexlem4d  13549  iscatd2  13583  drsdirfi  14072  issubg2  14636  subgint  14641  giclcl  14736  gicrcl  14737  gicsym  14738  gictr  14739  gicen  14741  gicsubgen  14742  cntzssv  14804  sylow1lem4  14912  odcau  14915  sylow3  14944  cyggex2  15183  giccyg  15186  pgpfac1lem5  15314  subrgint  15567  lss0cl  15704  lmiclcl  15823  lmicrcl  15824  lmicsym  15825  lspsnat  15898  lspprat  15906  abvn0b  16043  cnsubrg  16432  cygzn  16524  toponmre  16830  iunconlem  17153  iuncon  17154  uncon  17155  clscon  17156  2ndcdisj  17182  2ndcsep  17185  1stcelcls  17187  txcls  17299  hmphsym  17473  hmphtr  17474  hmphen  17476  haushmphlem  17478  cmphmph  17479  conhmph  17480  reghmph  17484  nrmhmph  17485  hmphdis  17487  hmphen2  17490  fbdmn0  17529  isfbas2  17530  fbssint  17533  trfbas2  17538  filtop  17550  isfil2  17551  elfg  17566  fgcl  17573  filssufilg  17606  uffix2  17619  ufildom1  17621  hauspwpwf1  17682  hausflf2  17693  alexsubALTlem2  17742  ptcmplem2  17747  tgptsmscld  17833  xbln0  17965  lpbl  18049  met2ndci  18068  reconn  18333  opnreen  18336  metdsre  18357  phtpcer  18493  phtpc01  18494  phtpcco2  18497  pcohtpy  18518  cfilfcls  18700  cmetcaulem  18714  cmetcau  18715  cmetss  18740  bcthlem5  18750  ovolicc2lem2  18877  ovolicc2lem5  18880  ioorcl2  18927  ioorinv2  18930  itg11  19046  dvlip  19340  dvne0  19358  mpfrcl  19402  fta1g  19553  plyssc  19582  fta1  19688  vieta1lem2  19691  isgrp2d  20902  ubthlem1  21449  shintcli  21908  esumcst  23436  insiga  23498  pconcon  23762  txscon  23772  cvmsss2  23805  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem2  23813  cvmlift2lem10  23843  cvmliftpht  23849  cvmlift3lem8  23857  umgraex  23875  eupath  23905  dedekind  24082  dedekindle  24083  eldm3  24119  fundmpss  24122  frmin  24242  nocvxmin  24345  axcontlem4  24595  axcontlem10  24601  prl  25167  dstr  25171  aline  26074  isconcl6a  26103  isconcl6ab  26104  lppotos  26144  bhp3  26177  locfincmp  26304  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  fnemeet2  26316  fnejoin2  26318  neifg  26320  tailfb  26326  filnetlem3  26329  prdsbnd2  26519  heibor1lem  26533  bfp  26548  divrngidl  26653  rencldnfilem  26903  kelac1  27161  lnmlmic  27186  gicabl  27263  lmiclbs  27307  lmisfree  27312  symggen  27411  psgnunilem3  27419  stoweidlem35  27784  nbusgra  28143  onfrALT  28314  onfrALTVD  28667  bnj521  28765  bnj1189  29039  bnj1279  29048  atex  29595  llnn0  29705  lplnn0N  29736  lvoln0N  29780  pmapglb2N  29960  pmapglb2xN  29961  elpaddn0  29989  osumcllem8N  30152  pexmidlem5N  30163  diaglbN  31245  diaintclN  31248  dibglbN  31356  dibintclN  31357  dihglblem2aN  31483  dihglblem5  31488  dihglbcpreN  31490  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator