Theorem n0 3744

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

Syntax hints:   <-> wb 184   E.wex 1587   e. wcel 1758   =/= wne 2644   (/)c0 3735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-v 3070  df-dif 3429  df-nul 3736

This theorem is referenced by:  neq0  3745  reximdva0  3746  rspn0  3747  n0moeu  3748  pssnel  3842  r19.2z  3867  r19.2zb  3868  r19.3rz  3869  r19.3rzv  3871  uniintsn  4263  iunn0  4328  trint0  4500  intex  4546  notzfaus  4565  reusv2lem1  4591  reusv5OLD  4600  nnullss  4652  exss  4653  opabn0  4717  wefrc  4812  wereu2  4815  onfr  4856  dmxp  5156  xpnz  5355  dmsnn0  5402  unixp0  5469  xpco  5475  eldmrexrnb  5949  isofrlem  6130  limuni3  6563  soex  6621  f1oweALT  6661  fo1stres  6700  fo2ndres  6701  ecdmn0  7243  map0g  7352  ixpn0  7395  resixpfo  7401  domdifsn  7494  xpdom3  7509  fodomr  7562  mapdom3  7583  findcard2  7653  unblem2  7666  marypha1lem  7784  brwdom2  7889  unxpwdom2  7904  ixpiunwdom  7907  zfreg  7911  zfreg2  7912  epfrs  8052  scott0  8194  cplem1  8197  fseqen  8298  finacn  8321  iunfictbso  8385  aceq2  8390  dfac3  8392  dfac9  8406  kmlem6  8425  kmlem8  8427  infpss  8487  fin23lem7  8586  enfin2i  8591  fin23lem21  8609  fin23lem31  8613  isf32lem9  8631  isf34lem4  8647  axdc2lem  8718  axdc3lem4  8723  ac6c4  8751  ac9  8753  ac6s4  8760  ac9s  8763  ttukeyg  8787  fpwwe2lem12  8909  wun0  8986  tsk0  9031  gruina  9086  genpn0  9273  prlem934  9303  ltaddpr  9304  ltexprlem1  9306  prlem936  9317  reclem2pr  9318  suplem1pr  9322  supsr  9380  axpre-sup  9437  dedekind  9634  dedekindle  9635  infm3  10390  supmul1  10396  supmullem2  10398  supmul  10399  infmrcl  10410  negn0  11042  zsupss  11045  xrsupsslem  11370  xrinfmsslem  11371  supxrre  11391  infmxrre  11399  ixxub  11422  ixxlb  11423  ioorebas  11492  fzn0  11565  fzon0  11670  hashgt0elexb  12262  swrdcl  12417  maxprmfct  13901  4sqlem12  14119  vdwmc  14141  ramz  14188  ramub1  14191  mreiincl  14636  mremre  14644  mreexexlem4d  14687  iscatd2  14721  drsdirfi  15210  issubg2  15798  subgint  15807  giclcl  15902  gicrcl  15903  gicsym  15904  gictr  15905  gicen  15907  gicsubgen  15908  cntzssv  15948  symggen  16078  psgnunilem3  16104  sylow1lem4  16204  odcau  16207  sylow3  16236  cyggex2  16477  giccyg  16480  pgpfac1lem5  16685  subrgint  16993  lss0cl  17134  lmiclcl  17257  lmicrcl  17258  lmicsym  17259  lspsnat  17332  lspprat  17340  abvn0b  17480  mpfrcl  17711  ply1frcl  17862  cnsubrg  17982  cygzn  18112  lmiclbs  18375  lmisfree  18380  lmictra  18383  mdetdiaglem  18520  mdet0  18528  toponmre  18813  iunconlem  19147  iuncon  19148  uncon  19149  clscon  19150  2ndcdisj  19176  2ndcsep  19179  1stcelcls  19181  txcls  19293  hmphsym  19471  hmphtr  19472  hmphen  19474  haushmphlem  19476  cmphmph  19477  conhmph  19478  reghmph  19482  nrmhmph  19483  hmphdis  19485  hmphen2  19488  fbdmn0  19523  isfbas2  19524  fbssint  19527  trfbas2  19532  filtop  19544  isfil2  19545  elfg  19560  fgcl  19567  filssufilg  19600  uffix2  19613  ufildom1  19615  hauspwpwf1  19676  hausflf2  19687  alexsubALTlem2  19736  ptcmplem2  19741  cnextf  19754  tgptsmscld  19841  ustfilxp  19903  xbln0  20105  lpbl  20194  met2ndci  20213  metustfbasOLD  20256  metustfbas  20257  restmetu  20278  reconn  20521  opnreen  20524  metdsre  20545  phtpcer  20683  phtpc01  20684  phtpcco2  20687  pcohtpy  20708  cfilfcls  20901  cmetcaulem  20915  cmetcau  20916  cmetss  20941  bcthlem5  20955  ovolicc2lem2  21117  ovolicc2lem5  21120  ioorcl2  21168  ioorinv2  21171  itg11  21285  dvlip  21581  dvne0  21599  fta1g  21755  plyssc  21784  fta1  21890  vieta1lem2  21893  axcontlem4  23348  axcontlem10  23354  umgraex  23392  eupath  23737  isgrp2d  23857  ubthlem1  24406  shintcli  24867  fpwrelmapffslem  26166  fmcncfil  26495  insiga  26714  pconcon  27254  txscon  27264  cvmsss2  27297  cvmopnlem  27301  cvmfolem  27302  cvmliftmolem2  27305  cvmlift2lem10  27335  cvmliftpht  27341  cvmlift3lem8  27349  eldm3  27706  fundmpss  27711  elima4  27724  frmin  27837  nocvxmin  27966  supaddc  28555  supadd  28556  itg2addnclem2  28582  locfincmp  28714  comppfsc  28717  neibastop1  28718  neibastop2lem  28719  neibastop2  28720  fnemeet2  28726  fnejoin2  28728  neifg  28730  tailfb  28736  filnetlem3  28739  prdsbnd2  28832  heibor1lem  28846  bfp  28861  divrngidl  28966  rencldnfilem  29297  kelac1  29554  lnmlmic  29579  gicabl  29592  stoweidlem35  29968  wlk0  30430  2spontn0vne  30544  usgn0fidegnn0  30760  frgrawopreglem2  30776  alscn0d  31447  onfrALT  31557  onfrALTVD  31927  iunconlem2  31971  bnj521  32028  bnj1189  32300  bnj1279  32309  bj-n0i  32738  atex  33356  llnn0  33466  lplnn0N  33497  lvoln0N  33541  pmapglb2N  33721  pmapglb2xN  33722  elpaddn0  33750  osumcllem8N  33913  pexmidlem5N  33924  diaglbN  35006  diaintclN  35009  dibglbN  35117  dibintclN  35118  dihglblem2aN  35244  dihglblem5  35249  dihglbcpreN  35251  dihintcl  35295