Theorem n0 3771

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 2584	. 2 |- F/_ x A
2	1	n0f 3770	1 |- ( A =/= (/) <-> E. x x e. A )

Syntax hints:   <-> wb 187   E.wex 1659   e. wcel 1868   =/= wne 2618   (/)c0 3761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-v 3083  df-dif 3439  df-nul 3762

This theorem is referenced by:  neq0  3772  reximdva0  3773  rspn0  3774  n0moeu  3775  pssnel  3860  r19.2z  3886  r19.2zb  3887  r19.3rz  3888  r19.3rzv  3890  uniintsn  4290  iunn0  4356  trint0  4532  intex  4577  notzfaus  4596  reusv2lem1  4622  nnullss  4680  exss  4681  opabn0  4748  wefrc  4844  wereu2  4847  dmxp  5069  xpnz  5272  dmsnn0  5317  unixp0  5386  xpco  5392  onfr  5478  fveqdmss  6029  eldmrexrnb  6041  isofrlem  6243  limuni3  6690  soex  6747  f1oweALT  6788  fo1stres  6828  fo2ndres  6829  ecdmn0  7411  map0g  7516  ixpn0  7559  resixpfo  7565  domdifsn  7658  xpdom3  7673  fodomr  7726  mapdom3  7747  findcard2  7814  unblem2  7827  marypha1lem  7950  brwdom2  8091  unxpwdom2  8106  ixpiunwdom  8109  zfreg  8113  zfreg2  8114  epfrs  8217  scott0  8359  cplem1  8362  fseqen  8459  finacn  8482  iunfictbso  8546  aceq2  8551  dfac3  8553  dfac9  8567  kmlem6  8586  kmlem8  8588  infpss  8648  fin23lem7  8747  enfin2i  8752  fin23lem21  8770  fin23lem31  8774  isf32lem9  8792  isf34lem4  8808  axdc2lem  8879  axdc3lem4  8884  ac6c4  8912  ac9  8914  ac6s4  8921  ac9s  8924  ttukeyg  8948  fpwwe2lem12  9067  wun0  9144  tsk0  9189  gruina  9244  genpn0  9429  prlem934  9459  ltaddpr  9460  ltexprlem1  9462  prlem936  9473  reclem2pr  9474  suplem1pr  9478  supsr  9537  axpre-sup  9594  dedekind  9798  dedekindle  9799  negn0  10049  infm3  10569  supaddc  10575  supadd  10576  supmul1  10577  supmullem2  10579  supmul  10580  infmrclOLD  10594  zsupss  11254  xrsupsslem  11593  xrinfmsslem  11594  supxrre  11614  infxrre  11623  infmxrreOLD  11627  ixxub  11657  ixxlb  11658  ixxlbOLD  11659  ioorebas  11737  fzn0  11814  fzon0  11938  hashgt0elexb  12579  swrdcl  12766  xpcogend  13027  maxprmfct  14640  4sqlem12  14888  vdwmc  14916  ramz  14971  ramub1  14974  mreiincl  15490  mremre  15498  mreexexlem4d  15541  iscatd2  15575  cic  15692  drsdirfi  16171  opifismgm  16489  issubg2  16820  subgint  16829  giclcl  16924  gicrcl  16925  gicsym  16926  gictr  16927  gicen  16929  gicsubgen  16930  cntzssv  16970  symggen  17099  psgnunilem3  17125  sylow1lem4  17241  odcau  17244  sylow3  17273  cyggex2  17519  giccyg  17522  pgpfac1lem5  17700  brric2  17961  subrgint  18018  lss0cl  18158  lmiclcl  18281  lmicrcl  18282  lmicsym  18283  lspsnat  18356  lspprat  18364  abvn0b  18514  mpfrcl  18729  ply1frcl  18895  cnsubrg  19016  cygzn  19128  lmiclbs  19382  lmisfree  19387  lmictra  19390  mdetdiaglem  19610  mdet0  19618  toponmre  20096  iunconlem  20429  iuncon  20430  uncon  20431  clscon  20432  2ndcdisj  20458  2ndcsep  20461  1stcelcls  20463  locfincmp  20528  comppfsc  20534  txcls  20606  hmphsym  20784  hmphtr  20785  hmphen  20787  haushmphlem  20789  cmphmph  20790  conhmph  20791  reghmph  20795  nrmhmph  20796  hmphdis  20798  hmphen2  20801  fbdmn0  20836  isfbas2  20837  fbssint  20840  trfbas2  20845  filtop  20857  isfil2  20858  elfg  20873  fgcl  20880  filssufilg  20913  uffix2  20926  ufildom1  20928  hauspwpwf1  20989  hausflf2  21000  alexsubALTlem2  21050  ptcmplem2  21055  cnextf  21068  tgptsmscld  21152  ustfilxp  21214  xbln0  21416  lpbl  21505  met2ndci  21524  metustfbas  21559  restmetu  21572  reconn  21833  opnreen  21836  metdsre  21857  metdsreOLD  21872  phtpcer  22013  phtpc01  22014  phtpcco2  22017  pcohtpy  22038  cfilfcls  22231  cmetcaulem  22245  cmetcau  22246  cmetss  22271  bcthlem5  22283  ovolicc2lem2  22458  ovolicc2lem5  22462  ioorcl2  22511  ioorinv2  22514  ioorinv2OLD  22519  itg11  22636  dvlip  22932  dvne0  22950  fta1g  23105  plyssc  23141  fta1  23248  vieta1lem2  23251  hpgerlem  24794  axcontlem4  24984  axcontlem10  24990  umgraex  25037  2spontn0vne  25601  eupath  25695  usgn0fidegnn0  25743  frgrawopreglem2  25759  isgrp2d  25949  ubthlem1  26498  shintcli  26968  fpwrelmapffslem  28311  fmcncfil  28733  insiga  28955  unelldsys  28976  bnj521  29541  bnj1189  29814  bnj1279  29823  pconcon  29950  txscon  29960  cvmsss2  29993  cvmopnlem  29997  cvmfolem  29998  cvmliftmolem2  30001  cvmlift2lem10  30031  cvmliftpht  30037  cvmlift3lem8  30045  eldm3  30397  fundmpss  30402  elima4  30416  frmin  30475  nocvxmin  30573  neibastop1  31008  neibastop2lem  31009  neibastop2  31010  fnemeet2  31016  fnejoin2  31018  neifg  31020  tailfb  31026  filnetlem3  31029  bj-n0i  31496  poimirlem30  31884  itg2addnclem2  31908  prdsbnd2  32041  heibor1lem  32055  bfp  32070  divrngidl  32175  atex  32890  llnn0  33000  lplnn0N  33031  lvoln0N  33075  pmapglb2N  33255  pmapglb2xN  33256  elpaddn0  33284  osumcllem8N  33447  pexmidlem5N  33458  diaglbN  34542  diaintclN  34545  dibglbN  34653  dibintclN  34654  dihglblem2aN  34780  dihglblem5  34785  dihglbcpreN  34787  dihintcl  34831  rencldnfilem  35582  kelac1  35841  lnmlmic  35866  gicabl  35877  ndisj  36222  onfrALT  36773  onfrALTVD  37149  iunconlem2  37193  suprnmpt  37288  disjinfi  37318  infrpge  37416  inficc  37466  fsumnncl  37473  ellimciota  37514  islpcn  37539  lptre2pt  37540  stoweidlem35  37716  fourierdlem31  37820  fourierdlem31OLD  37821  fourier2  37911  intsaluni  37989  sge0cl  38011  ovn0lem  38162  ovnsubaddlem2  38168  pfxcl  38639  umgrex  38845  mgmpropd  39047  opmpt2ismgm  39079  nzerooringczr  39346  alscn0d  39808