Theorem n0 3597

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

Step	Hyp	Ref	Expression
1		nfcv 2540	. 2 |- F/_ x A
2	1	n0f 3596	1 |- ( A =/= (/) <-> E. x x e. A )

Syntax hints:   <-> wb 177   E.wex 1547   e. wcel 1721   =/= wne 2567   (/)c0 3588

This theorem is referenced by:  neq0  3598  reximdva0  3599  n0moeu  3600  pssnel  3653  r19.2z  3677  r19.2zb  3678  r19.3rz  3679  r19.3rzv  3681  uniintsn  4047  iunn0  4111  trint0  4279  intex  4316  notzfaus  4334  nnullss  4385  exss  4386  opabn0  4445  wefrc  4536  wereu2  4539  onfr  4580  reusv2lem1  4683  reusv5OLD  4692  limuni3  4791  dmxp  5047  xpnz  5251  soex  5278  dmsnn0  5294  unixp0  5362  xpco  5373  eldmrexrnb  5836  isofrlem  6019  f1oweALT  6033  fo1stres  6329  fo2ndres  6330  ecdmn0  6906  map0g  7012  ixpn0  7053  resixpfo  7059  domdifsn  7150  xpdom3  7165  fodomr  7217  mapdom3  7238  findcard2  7307  unblem2  7319  marypha1lem  7396  brwdom2  7497  unxpwdom2  7512  ixpiunwdom  7515  zfreg  7519  zfreg2  7520  epfrs  7623  scott0  7766  cplem1  7769  fseqen  7864  finacn  7887  iunfictbso  7951  aceq2  7956  dfac3  7958  dfac9  7972  kmlem6  7991  kmlem8  7993  infpss  8053  fin23lem7  8152  enfin2i  8157  fin23lem21  8175  fin23lem31  8179  isf32lem9  8197  isf34lem4  8213  axdc2lem  8284  axdc3lem4  8289  ac6c4  8317  ac9  8319  ac6s4  8326  ac9s  8329  ttukeyg  8353  fpwwe2lem12  8472  wun0  8549  tsk0  8594  gruina  8649  genpn0  8836  prlem934  8866  ltaddpr  8867  ltexprlem1  8869  prlem936  8880  reclem2pr  8881  suplem1pr  8885  supsr  8943  axpre-sup  9000  infm3  9923  supmul1  9929  supmullem2  9931  supmul  9932  infmrcl  9943  negn0  10518  zsupss  10521  xrsupsslem  10841  xrinfmsslem  10842  supxrre  10862  infmxrre  10870  ixxub  10893  ixxlb  10894  ioorebas  10962  fzn0  11026  fzon0  11111  hashgt0elexb  11626  swrdcl  11721  maxprmfct  13068  4sqlem12  13279  vdwmc  13301  ramz  13348  ramub1  13351  mreiincl  13776  mremre  13784  mreexexlem4d  13827  iscatd2  13861  drsdirfi  14350  issubg2  14914  subgint  14919  giclcl  15014  gicrcl  15015  gicsym  15016  gictr  15017  gicen  15019  gicsubgen  15020  cntzssv  15082  sylow1lem4  15190  odcau  15193  sylow3  15222  cyggex2  15461  giccyg  15464  pgpfac1lem5  15592  subrgint  15845  lss0cl  15978  lmiclcl  16097  lmicrcl  16098  lmicsym  16099  lspsnat  16172  lspprat  16180  abvn0b  16317  cnsubrg  16714  cygzn  16806  toponmre  17112  iunconlem  17443  iuncon  17444  uncon  17445  clscon  17446  2ndcdisj  17472  2ndcsep  17475  1stcelcls  17477  txcls  17589  hmphsym  17767  hmphtr  17768  hmphen  17770  haushmphlem  17772  cmphmph  17773  conhmph  17774  reghmph  17778  nrmhmph  17779  hmphdis  17781  hmphen2  17784  fbdmn0  17819  isfbas2  17820  fbssint  17823  trfbas2  17828  filtop  17840  isfil2  17841  elfg  17856  fgcl  17863  filssufilg  17896  uffix2  17909  ufildom1  17911  hauspwpwf1  17972  hausflf2  17983  alexsubALTlem2  18032  ptcmplem2  18037  cnextf  18050  tgptsmscld  18133  ustfilxp  18195  xbln0  18397  lpbl  18486  met2ndci  18505  metustfbasOLD  18548  metustfbas  18549  restmetu  18570  reconn  18812  opnreen  18815  metdsre  18836  phtpcer  18973  phtpc01  18974  phtpcco2  18977  pcohtpy  18998  cfilfcls  19180  cmetcaulem  19194  cmetcau  19195  cmetss  19220  bcthlem5  19234  ovolicc2lem2  19367  ovolicc2lem5  19370  ioorcl2  19417  ioorinv2  19420  itg11  19536  dvlip  19830  dvne0  19848  mpfrcl  19892  fta1g  20043  plyssc  20072  fta1  20178  vieta1lem2  20181  umgraex  21311  eupath  21656  isgrp2d  21776  ubthlem1  22325  shintcli  22784  fmcncfil  24270  insiga  24473  pconcon  24871  txscon  24881  cvmsss2  24914  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem2  24922  cvmlift2lem10  24952  cvmliftpht  24958  cvmlift3lem8  24966  dedekind  25140  dedekindle  25141  eldm3  25333  fundmpss  25336  frmin  25456  nocvxmin  25559  axcontlem4  25810  axcontlem10  25816  supaddc  26137  supadd  26138  itg2addnclem2  26156  locfincmp  26274  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  fnemeet2  26286  fnejoin2  26288  neifg  26290  tailfb  26296  filnetlem3  26299  prdsbnd2  26394  heibor1lem  26408  bfp  26423  divrngidl  26528  rencldnfilem  26771  kelac1  27029  lnmlmic  27054  gicabl  27131  lmiclbs  27175  lmisfree  27180  symggen  27279  psgnunilem3  27287  stoweidlem35  27651  2spontn0vne  28084  frgrawopreglem2  28148  onfrALT  28346  onfrALTVD  28712  bnj521  28810  bnj1189  29084  bnj1279  29093  atex  29888  llnn0  29998  lplnn0N  30029  lvoln0N  30073  pmapglb2N  30253  pmapglb2xN  30254  elpaddn0  30282  osumcllem8N  30445  pexmidlem5N  30456  diaglbN  31538  diaintclN  31541  dibglbN  31649  dibintclN  31650  dihglblem2aN  31776  dihglblem5  31781  dihglbcpreN  31783  dihintcl  31827

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 2385

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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-nul 3589