Theorem n0 3741

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

Syntax hints:   <-> wb 188   E.wex 1663   e. wcel 1887   =/= wne 2622   (/)c0 3731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-v 3047  df-dif 3407  df-nul 3732

This theorem is referenced by:  neq0  3742  reximdva0  3743  rspn0  3744  n0moeu  3745  pssnel  3832  r19.2z  3858  r19.2zb  3859  r19.3rz  3860  r19.3rzv  3862  uniintsn  4272  iunn0  4338  trint0  4514  intex  4559  notzfaus  4578  reusv2lem1  4604  nnullss  4662  exss  4663  opabn0  4732  wefrc  4828  wereu2  4831  dmxp  5053  xpnz  5256  dmsnn0  5301  unixp0  5370  xpco  5376  onfr  5462  fveqdmss  6017  eldmrexrnb  6029  isofrlem  6231  limuni3  6679  soex  6736  f1oweALT  6777  fo1stres  6817  fo2ndres  6818  ecdmn0  7406  map0g  7511  ixpn0  7554  resixpfo  7560  domdifsn  7655  xpdom3  7670  fodomr  7723  mapdom3  7744  findcard2  7811  unblem2  7824  marypha1lem  7947  brwdom2  8088  unxpwdom2  8103  ixpiunwdom  8106  zfreg  8110  zfreg2  8111  epfrs  8215  scott0  8357  cplem1  8360  fseqen  8458  finacn  8481  iunfictbso  8545  aceq2  8550  dfac3  8552  dfac9  8566  kmlem6  8585  kmlem8  8587  infpss  8647  fin23lem7  8746  enfin2i  8751  fin23lem21  8769  fin23lem31  8773  isf32lem9  8791  isf34lem4  8807  axdc2lem  8878  axdc3lem4  8883  ac6c4  8911  ac9  8913  ac6s4  8920  ac9s  8923  ttukeyg  8947  fpwwe2lem12  9066  wun0  9143  tsk0  9188  gruina  9243  genpn0  9428  prlem934  9458  ltaddpr  9459  ltexprlem1  9461  prlem936  9472  reclem2pr  9473  suplem1pr  9477  supsr  9536  axpre-sup  9593  dedekind  9797  dedekindle  9798  negn0  10048  infm3  10568  supaddc  10574  supadd  10575  supmul1  10576  supmullem2  10578  supmul  10579  infmrclOLD  10593  zsupss  11253  xrsupsslem  11592  xrinfmsslem  11593  supxrre  11613  infxrre  11622  infmxrreOLD  11626  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  ioorebas  11736  fzn0  11813  fzon0  11937  hashgt0elexb  12579  swrdcl  12775  xpcogend  13038  maxprmfct  14652  4sqlem12  14900  vdwmc  14928  ramz  14983  ramub1  14986  mreiincl  15502  mremre  15510  mreexexlem4d  15553  iscatd2  15587  cic  15704  drsdirfi  16183  opifismgm  16501  issubg2  16832  subgint  16841  giclcl  16936  gicrcl  16937  gicsym  16938  gictr  16939  gicen  16941  gicsubgen  16942  cntzssv  16982  symggen  17111  psgnunilem3  17137  sylow1lem4  17253  odcau  17256  sylow3  17285  cyggex2  17531  giccyg  17534  pgpfac1lem5  17712  brric2  17973  subrgint  18030  lss0cl  18170  lmiclcl  18293  lmicrcl  18294  lmicsym  18295  lspsnat  18368  lspprat  18376  abvn0b  18526  mpfrcl  18741  ply1frcl  18907  cnsubrg  19028  cygzn  19141  lmiclbs  19395  lmisfree  19400  lmictra  19403  mdetdiaglem  19623  mdet0  19631  toponmre  20109  iunconlem  20442  iuncon  20443  uncon  20444  clscon  20445  2ndcdisj  20471  2ndcsep  20474  1stcelcls  20476  locfincmp  20541  comppfsc  20547  txcls  20619  hmphsym  20797  hmphtr  20798  hmphen  20800  haushmphlem  20802  cmphmph  20803  conhmph  20804  reghmph  20808  nrmhmph  20809  hmphdis  20811  hmphen2  20814  fbdmn0  20849  isfbas2  20850  fbssint  20853  trfbas2  20858  filtop  20870  isfil2  20871  elfg  20886  fgcl  20893  filssufilg  20926  uffix2  20939  ufildom1  20941  hauspwpwf1  21002  hausflf2  21013  alexsubALTlem2  21063  ptcmplem2  21068  cnextf  21081  tgptsmscld  21165  ustfilxp  21227  xbln0  21429  lpbl  21518  met2ndci  21537  metustfbas  21572  restmetu  21585  reconn  21846  opnreen  21849  metdsre  21870  metdsreOLD  21885  phtpcer  22026  phtpc01  22027  phtpcco2  22030  pcohtpy  22051  cfilfcls  22244  cmetcaulem  22258  cmetcau  22259  cmetss  22284  bcthlem5  22296  ovolicc2lem2  22471  ovolicc2lem5  22475  ioorcl2  22524  ioorinv2  22527  ioorinv2OLD  22532  itg11  22649  dvlip  22945  dvne0  22963  fta1g  23118  plyssc  23154  fta1  23261  vieta1lem2  23264  hpgerlem  24807  axcontlem4  24997  axcontlem10  25003  umgraex  25050  2spontn0vne  25615  eupath  25709  usgn0fidegnn0  25757  frgrawopreglem2  25773  isgrp2d  25963  ubthlem1  26512  shintcli  26982  fpwrelmapffslem  28317  fmcncfil  28737  insiga  28959  unelldsys  28980  bnj521  29545  bnj1189  29818  bnj1279  29827  pconcon  29954  txscon  29964  cvmsss2  29997  cvmopnlem  30001  cvmfolem  30002  cvmliftmolem2  30005  cvmlift2lem10  30035  cvmliftpht  30041  cvmlift3lem8  30049  eldm3  30402  fundmpss  30407  elima4  30421  frmin  30480  nocvxmin  30580  neibastop1  31015  neibastop2lem  31016  neibastop2  31017  fnemeet2  31023  fnejoin2  31025  neifg  31027  tailfb  31033  filnetlem3  31036  bj-n0i  31540  poimirlem30  31970  itg2addnclem2  31994  prdsbnd2  32127  heibor1lem  32141  bfp  32156  divrngidl  32261  atex  32971  llnn0  33081  lplnn0N  33112  lvoln0N  33156  pmapglb2N  33336  pmapglb2xN  33337  elpaddn0  33365  osumcllem8N  33528  pexmidlem5N  33539  diaglbN  34623  diaintclN  34626  dibglbN  34734  dibintclN  34735  dihglblem2aN  34861  dihglblem5  34866  dihglbcpreN  34868  dihintcl  34912  rencldnfilem  35663  kelac1  35921  lnmlmic  35946  gicabl  35957  ndisj  36364  onfrALT  36915  onfrALTVD  37288  iunconlem2  37332  suprnmpt  37439  disjinfi  37468  infrpge  37574  inficc  37636  fsumnncl  37650  ellimciota  37694  islpcn  37719  lptre2pt  37720  stoweidlem35  37896  fourierdlem31  38000  fourierdlem31OLD  38001  fourier2  38091  qndenserrnbllem  38163  qndenserrnopn  38167  qndenserrn  38168  intsaluni  38188  sge0cl  38223  ovn0lem  38387  ovnsubaddlem2  38393  hoidmvval0b  38412  hspdifhsp  38438  pfxcl  38927  n0rex  38988  upgrex  39184  uhgrvd00  39571  mgmpropd  39828  opmpt2ismgm  39860  nzerooringczr  40127  alscn0d  40587