Theorem n0 3732

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

Syntax hints:   <-> wb 189   E.wex 1671   e. wcel 1904   =/= wne 2641   (/)c0 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-v 3033  df-dif 3393  df-nul 3723

This theorem is referenced by:  neq0  3733  reximdva0  3734  rspn0  3735  n0moeu  3736  pssnel  3829  r19.2z  3849  r19.2zb  3850  r19.3rz  3851  r19.3rzv  3853  uniintsn  4263  iunn0  4329  trint0  4507  intex  4557  notzfaus  4576  reusv2lem1  4602  nnullss  4662  exss  4663  opabn0  4732  wefrc  4833  wereu2  4836  dmxp  5059  xpnz  5262  dmsnn0  5308  unixp0  5377  xpco  5383  onfr  5469  fveqdmss  6032  eldmrexrnb  6044  isofrlem  6249  limuni3  6698  soex  6755  f1oweALT  6796  fo1stres  6836  fo2ndres  6837  ecdmn0  7424  map0g  7529  ixpn0  7572  resixpfo  7578  domdifsn  7673  xpdom3  7688  fodomr  7741  mapdom3  7762  findcard2  7829  unblem2  7842  marypha1lem  7965  brwdom2  8106  unxpwdom2  8121  ixpiunwdom  8124  zfreg  8128  zfreg2  8129  epfrs  8233  scott0  8375  cplem1  8378  fseqen  8476  finacn  8499  iunfictbso  8563  aceq2  8568  dfac3  8570  dfac9  8584  kmlem6  8603  kmlem8  8605  infpss  8665  fin23lem7  8764  enfin2i  8769  fin23lem21  8787  fin23lem31  8791  isf32lem9  8809  isf34lem4  8825  axdc2lem  8896  axdc3lem4  8901  ac6c4  8929  ac9  8931  ac6s4  8938  ac9s  8941  ttukeyg  8965  fpwwe2lem12  9084  wun0  9161  tsk0  9206  gruina  9261  genpn0  9446  prlem934  9476  ltaddpr  9477  ltexprlem1  9479  prlem936  9490  reclem2pr  9491  suplem1pr  9495  supsr  9554  axpre-sup  9611  dedekind  9815  dedekindle  9816  negn0  10069  infm3  10590  supaddc  10596  supadd  10597  supmul1  10598  supmullem2  10600  supmul  10601  infmrclOLD  10615  zsupss  11276  xrsupsslem  11617  xrinfmsslem  11618  supxrre  11638  infxrre  11647  infmxrreOLD  11651  ixxub  11681  ixxlb  11682  ixxlbOLD  11683  ioorebas  11761  fzn0  11839  fzon0  11964  hashgt0elexb  12617  swrdcl  12829  xpcogend  13113  maxprmfct  14731  4sqlem12  14979  vdwmc  15007  ramz  15062  ramub1  15065  mreiincl  15580  mremre  15588  mreexexlem4d  15631  iscatd2  15665  cic  15782  drsdirfi  16261  opifismgm  16579  issubg2  16910  subgint  16919  giclcl  17014  gicrcl  17015  gicsym  17016  gictr  17017  gicen  17019  gicsubgen  17020  cntzssv  17060  symggen  17189  psgnunilem3  17215  sylow1lem4  17331  odcau  17334  sylow3  17363  cyggex2  17609  giccyg  17612  pgpfac1lem5  17790  brric2  18051  subrgint  18108  lss0cl  18248  lmiclcl  18371  lmicrcl  18372  lmicsym  18373  lspsnat  18446  lspprat  18454  abvn0b  18603  mpfrcl  18818  ply1frcl  18984  cnsubrg  19105  cygzn  19218  lmiclbs  19472  lmisfree  19477  lmictra  19480  mdetdiaglem  19700  mdet0  19708  toponmre  20186  iunconlem  20519  iuncon  20520  uncon  20521  clscon  20522  2ndcdisj  20548  2ndcsep  20551  1stcelcls  20553  locfincmp  20618  comppfsc  20624  txcls  20696  hmphsym  20874  hmphtr  20875  hmphen  20877  haushmphlem  20879  cmphmph  20880  conhmph  20881  reghmph  20885  nrmhmph  20886  hmphdis  20888  hmphen2  20891  fbdmn0  20927  isfbas2  20928  fbssint  20931  trfbas2  20936  filtop  20948  isfil2  20949  elfg  20964  fgcl  20971  filssufilg  21004  uffix2  21017  ufildom1  21019  hauspwpwf1  21080  hausflf2  21091  alexsubALTlem2  21141  ptcmplem2  21146  cnextf  21159  tgptsmscld  21243  ustfilxp  21305  xbln0  21507  lpbl  21596  met2ndci  21615  metustfbas  21650  restmetu  21663  reconn  21924  opnreen  21927  metdsre  21948  metdsreOLD  21963  phtpcer  22104  phtpc01  22105  phtpcco2  22108  pcohtpy  22129  cfilfcls  22322  cmetcaulem  22336  cmetcau  22337  cmetss  22362  bcthlem5  22374  ovolicc2lem2  22549  ovolicc2lem5  22553  ioorcl2  22603  ioorinv2  22606  ioorinv2OLD  22611  itg11  22728  dvlip  23024  dvne0  23042  fta1g  23197  plyssc  23233  fta1  23340  vieta1lem2  23343  hpgerlem  24886  axcontlem4  25076  axcontlem10  25082  umgraex  25129  2spontn0vne  25694  eupath  25788  usgn0fidegnn0  25836  frgrawopreglem2  25852  isgrp2d  26044  ubthlem1  26593  shintcli  27063  fpwrelmapffslem  28392  fmcncfil  28811  insiga  29033  unelldsys  29054  bnj521  29617  bnj1189  29890  bnj1279  29899  pconcon  30026  txscon  30036  cvmsss2  30069  cvmopnlem  30073  cvmfolem  30074  cvmliftmolem2  30077  cvmlift2lem10  30107  cvmliftpht  30113  cvmlift3lem8  30121  eldm3  30473  fundmpss  30478  elima4  30492  frmin  30551  nocvxmin  30651  neibastop1  31086  neibastop2lem  31087  neibastop2  31088  fnemeet2  31094  fnejoin2  31096  neifg  31098  tailfb  31104  filnetlem3  31107  bj-n0i  31610  poimirlem30  32034  itg2addnclem2  32058  prdsbnd2  32191  heibor1lem  32205  bfp  32220  divrngidl  32325  atex  33042  llnn0  33152  lplnn0N  33183  lvoln0N  33227  pmapglb2N  33407  pmapglb2xN  33408  elpaddn0  33436  osumcllem8N  33599  pexmidlem5N  33610  diaglbN  34694  diaintclN  34697  dibglbN  34805  dibintclN  34806  dihglblem2aN  34932  dihglblem5  34937  dihglbcpreN  34939  dihintcl  34983  rencldnfilem  35734  kelac1  35992  lnmlmic  36017  gicabl  36028  ndisj  36435  onfrALT  36985  onfrALTVD  37351  iunconlem2  37395  snelmap  37489  suprnmpt  37512  disjinfi  37539  mapss2  37557  difmap  37559  infrpge  37661  inficc  37732  fsumnncl  37746  ellimciota  37791  islpcn  37816  lptre2pt  37817  stoweidlem35  38008  fourierdlem31  38112  fourierdlem31OLD  38113  fourier2  38203  qndenserrnbllem  38275  qndenserrnopn  38279  qndenserrn  38280  intsaluni  38300  sge0cl  38337  ovn0lem  38505  ovnsubaddlem2  38511  hoidmvval0b  38530  hspdifhsp  38556  pfxcl  39074  n0rex  39135  upgrex  39338  uhgrvd00  39757  eulerpath  40153  mgmpropd  40283  opmpt2ismgm  40315  nzerooringczr  40582  alscn0d  41040