Theorem n0 3748

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

Syntax hints:   <-> wb 184   E.wex 1633   e. wcel 1842   =/= wne 2598   (/)c0 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3061  df-dif 3417  df-nul 3739

This theorem is referenced by:  neq0  3749  reximdva0  3750  rspn0  3751  n0moeu  3752  pssnel  3837  r19.2z  3862  r19.2zb  3863  r19.3rz  3864  r19.3rzv  3866  uniintsn  4265  iunn0  4331  trint0  4506  intex  4550  notzfaus  4569  reusv2lem1  4595  nnullss  4653  exss  4654  opabn0  4721  wefrc  4817  wereu2  4820  dmxp  5042  xpnz  5244  dmsnn0  5289  unixp0  5358  xpco  5364  onfr  5449  fveqdmss  6004  eldmrexrnb  6016  isofrlem  6219  limuni3  6670  soex  6727  f1oweALT  6768  fo1stres  6808  fo2ndres  6809  ecdmn0  7391  map0g  7496  ixpn0  7539  resixpfo  7545  domdifsn  7638  xpdom3  7653  fodomr  7706  mapdom3  7727  findcard2  7794  unblem2  7807  marypha1lem  7927  brwdom2  8033  unxpwdom2  8048  ixpiunwdom  8051  zfreg  8055  zfreg2  8056  epfrs  8194  scott0  8336  cplem1  8339  fseqen  8440  finacn  8463  iunfictbso  8527  aceq2  8532  dfac3  8534  dfac9  8548  kmlem6  8567  kmlem8  8569  infpss  8629  fin23lem7  8728  enfin2i  8733  fin23lem21  8751  fin23lem31  8755  isf32lem9  8773  isf34lem4  8789  axdc2lem  8860  axdc3lem4  8865  ac6c4  8893  ac9  8895  ac6s4  8902  ac9s  8905  ttukeyg  8929  fpwwe2lem12  9049  wun0  9126  tsk0  9171  gruina  9226  genpn0  9411  prlem934  9441  ltaddpr  9442  ltexprlem1  9444  prlem936  9455  reclem2pr  9456  suplem1pr  9460  supsr  9519  axpre-sup  9576  dedekind  9778  dedekindle  9779  infm3  10542  supmul1  10548  supmullem2  10550  supmul  10551  infmrcl  10562  negn0  11213  zsupss  11216  xrsupsslem  11551  xrinfmsslem  11552  supxrre  11572  infmxrre  11580  ixxub  11603  ixxlb  11604  ioorebas  11680  fzn0  11754  fzon0  11876  hashgt0elexb  12516  swrdcl  12700  xpcogend  12957  maxprmfct  14463  4sqlem12  14683  vdwmc  14705  ramz  14752  ramub1  14755  mreiincl  15210  mremre  15218  mreexexlem4d  15261  iscatd2  15295  cic  15412  drsdirfi  15891  opifismgm  16209  issubg2  16540  subgint  16549  giclcl  16644  gicrcl  16645  gicsym  16646  gictr  16647  gicen  16649  gicsubgen  16650  cntzssv  16690  symggen  16819  psgnunilem3  16845  sylow1lem4  16945  odcau  16948  sylow3  16977  cyggex2  17223  giccyg  17226  pgpfac1lem5  17450  brric2  17714  subrgint  17771  lss0cl  17913  lmiclcl  18036  lmicrcl  18037  lmicsym  18038  lspsnat  18111  lspprat  18119  abvn0b  18271  mpfrcl  18507  ply1frcl  18675  cnsubrg  18798  cygzn  18907  lmiclbs  19164  lmisfree  19169  lmictra  19172  mdetdiaglem  19392  mdet0  19400  toponmre  19887  iunconlem  20220  iuncon  20221  uncon  20222  clscon  20223  2ndcdisj  20249  2ndcsep  20252  1stcelcls  20254  locfincmp  20319  comppfsc  20325  txcls  20397  hmphsym  20575  hmphtr  20576  hmphen  20578  haushmphlem  20580  cmphmph  20581  conhmph  20582  reghmph  20586  nrmhmph  20587  hmphdis  20589  hmphen2  20592  fbdmn0  20627  isfbas2  20628  fbssint  20631  trfbas2  20636  filtop  20648  isfil2  20649  elfg  20664  fgcl  20671  filssufilg  20704  uffix2  20717  ufildom1  20719  hauspwpwf1  20780  hausflf2  20791  alexsubALTlem2  20840  ptcmplem2  20845  cnextf  20858  tgptsmscld  20945  ustfilxp  21007  xbln0  21209  lpbl  21298  met2ndci  21317  metustfbasOLD  21360  metustfbas  21361  restmetu  21382  reconn  21625  opnreen  21628  metdsre  21649  phtpcer  21787  phtpc01  21788  phtpcco2  21791  pcohtpy  21812  cfilfcls  22005  cmetcaulem  22019  cmetcau  22020  cmetss  22045  bcthlem5  22059  ovolicc2lem2  22221  ovolicc2lem5  22224  ioorcl2  22273  ioorinv2  22276  itg11  22390  dvlip  22686  dvne0  22704  fta1g  22860  plyssc  22889  fta1  22996  vieta1lem2  22999  hpgerlem  24522  axcontlem4  24687  axcontlem10  24693  umgraex  24740  2spontn0vne  25304  eupath  25398  usgn0fidegnn0  25446  frgrawopreglem2  25462  isgrp2d  25651  ubthlem1  26200  shintcli  26661  fpwrelmapffslem  28002  fmcncfil  28366  insiga  28585  unelldsys  28606  bnj521  29119  bnj1189  29392  bnj1279  29401  pconcon  29528  txscon  29538  cvmsss2  29571  cvmopnlem  29575  cvmfolem  29576  cvmliftmolem2  29579  cvmlift2lem10  29609  cvmliftpht  29615  cvmlift3lem8  29623  eldm3  29975  fundmpss  29980  elima4  29994  frmin  30053  nocvxmin  30151  neibastop1  30587  neibastop2lem  30588  neibastop2  30589  fnemeet2  30595  fnejoin2  30597  neifg  30599  tailfb  30605  filnetlem3  30608  bj-n0i  31068  supaddc  31413  supadd  31414  itg2addnclem2  31440  prdsbnd2  31573  heibor1lem  31587  bfp  31602  divrngidl  31707  atex  32423  llnn0  32533  lplnn0N  32564  lvoln0N  32608  pmapglb2N  32788  pmapglb2xN  32789  elpaddn0  32817  osumcllem8N  32980  pexmidlem5N  32991  diaglbN  34075  diaintclN  34078  dibglbN  34186  dibintclN  34187  dihglblem2aN  34313  dihglblem5  34318  dihglbcpreN  34320  dihintcl  34364  rencldnfilem  35115  kelac1  35371  lnmlmic  35396  gicabl  35411  ndisj  35749  onfrALT  36345  onfrALTVD  36722  iunconlem2  36766  suprnmpt  36826  fsumnncl  36940  ellimciota  36988  islpcn  37013  lptre2pt  37014  stoweidlem35  37185  fourierdlem31  37288  fourier2  37378  pfxcl  37873  mgmpropd  38092  opmpt2ismgm  38124  nzerooringczr  38391  alscn0d  38854