Theorem n0 3803

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

Syntax hints:   <-> wb 184   E.wex 1613   e. wcel 1819   =/= wne 2652   (/)c0 3793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-nul 3794

This theorem is referenced by:  neq0  3804  reximdva0  3805  rspn0  3806  n0moeu  3807  pssnel  3896  r19.2z  3921  r19.2zb  3922  r19.3rz  3923  r19.3rzv  3925  uniintsn  4326  iunn0  4392  trint0  4567  intex  4612  notzfaus  4631  reusv2lem1  4657  reusv5OLD  4666  nnullss  4718  exss  4719  opabn0  4787  wefrc  4882  wereu2  4885  onfr  4926  dmxp  5231  xpnz  5433  dmsnn0  5479  unixp0  5547  xpco  5553  fveqdmss  6027  eldmrexrnb  6039  isofrlem  6237  limuni3  6686  soex  6742  f1oweALT  6783  fo1stres  6823  fo2ndres  6824  ecdmn0  7372  map0g  7477  ixpn0  7520  resixpfo  7526  domdifsn  7619  xpdom3  7634  fodomr  7687  mapdom3  7708  findcard2  7778  unblem2  7791  marypha1lem  7911  brwdom2  8017  unxpwdom2  8032  ixpiunwdom  8035  zfreg  8039  zfreg2  8040  epfrs  8179  scott0  8321  cplem1  8324  fseqen  8425  finacn  8448  iunfictbso  8512  aceq2  8517  dfac3  8519  dfac9  8533  kmlem6  8552  kmlem8  8554  infpss  8614  fin23lem7  8713  enfin2i  8718  fin23lem21  8736  fin23lem31  8740  isf32lem9  8758  isf34lem4  8774  axdc2lem  8845  axdc3lem4  8850  ac6c4  8878  ac9  8880  ac6s4  8887  ac9s  8890  ttukeyg  8914  fpwwe2lem12  9036  wun0  9113  tsk0  9158  gruina  9213  genpn0  9398  prlem934  9428  ltaddpr  9429  ltexprlem1  9431  prlem936  9442  reclem2pr  9443  suplem1pr  9447  supsr  9506  axpre-sup  9563  dedekind  9761  dedekindle  9762  infm3  10522  supmul1  10528  supmullem2  10530  supmul  10531  infmrcl  10542  negn0  11193  zsupss  11196  xrsupsslem  11523  xrinfmsslem  11524  supxrre  11544  infmxrre  11552  ixxub  11575  ixxlb  11576  ioorebas  11651  fzn0  11725  fzon0  11843  hashgt0elexb  12471  swrdcl  12655  maxprmfct  14266  4sqlem12  14486  vdwmc  14508  ramz  14555  ramub1  14558  mreiincl  15013  mremre  15021  mreexexlem4d  15064  iscatd2  15098  cic  15215  drsdirfi  15694  opifismgm  16012  issubg2  16343  subgint  16352  giclcl  16447  gicrcl  16448  gicsym  16449  gictr  16450  gicen  16452  gicsubgen  16453  cntzssv  16493  symggen  16622  psgnunilem3  16648  sylow1lem4  16748  odcau  16751  sylow3  16780  cyggex2  17026  giccyg  17029  pgpfac1lem5  17257  brric2  17521  subrgint  17578  lss0cl  17720  lmiclcl  17843  lmicrcl  17844  lmicsym  17845  lspsnat  17918  lspprat  17926  abvn0b  18078  mpfrcl  18314  ply1frcl  18482  cnsubrg  18605  cygzn  18736  lmiclbs  18999  lmisfree  19004  lmictra  19007  mdetdiaglem  19227  mdet0  19235  toponmre  19721  iunconlem  20054  iuncon  20055  uncon  20056  clscon  20057  2ndcdisj  20083  2ndcsep  20086  1stcelcls  20088  locfincmp  20153  comppfsc  20159  txcls  20231  hmphsym  20409  hmphtr  20410  hmphen  20412  haushmphlem  20414  cmphmph  20415  conhmph  20416  reghmph  20420  nrmhmph  20421  hmphdis  20423  hmphen2  20426  fbdmn0  20461  isfbas2  20462  fbssint  20465  trfbas2  20470  filtop  20482  isfil2  20483  elfg  20498  fgcl  20505  filssufilg  20538  uffix2  20551  ufildom1  20553  hauspwpwf1  20614  hausflf2  20625  alexsubALTlem2  20674  ptcmplem2  20679  cnextf  20692  tgptsmscld  20779  ustfilxp  20841  xbln0  21043  lpbl  21132  met2ndci  21151  metustfbasOLD  21194  metustfbas  21195  restmetu  21216  reconn  21459  opnreen  21462  metdsre  21483  phtpcer  21621  phtpc01  21622  phtpcco2  21625  pcohtpy  21646  cfilfcls  21839  cmetcaulem  21853  cmetcau  21854  cmetss  21879  bcthlem5  21893  ovolicc2lem2  22055  ovolicc2lem5  22058  ioorcl2  22107  ioorinv2  22110  itg11  22224  dvlip  22520  dvne0  22538  fta1g  22694  plyssc  22723  fta1  22830  vieta1lem2  22833  hpgerlem  24260  axcontlem4  24397  axcontlem10  24403  umgraex  24450  2spontn0vne  25014  eupath  25108  usgn0fidegnn0  25156  frgrawopreglem2  25172  isgrp2d  25364  ubthlem1  25913  shintcli  26374  fpwrelmapffslem  27712  fmcncfil  28074  insiga  28310  pconcon  28873  txscon  28883  cvmsss2  28916  cvmopnlem  28920  cvmfolem  28921  cvmliftmolem2  28924  cvmlift2lem10  28954  cvmliftpht  28960  cvmlift3lem8  28968  eldm3  29409  fundmpss  29414  elima4  29426  frmin  29539  nocvxmin  29668  supaddc  30246  supadd  30247  itg2addnclem2  30272  neibastop1  30382  neibastop2lem  30383  neibastop2  30384  fnemeet2  30390  fnejoin2  30392  neifg  30394  tailfb  30400  filnetlem3  30403  prdsbnd2  30496  heibor1lem  30510  bfp  30525  divrngidl  30630  rencldnfilem  30958  kelac1  31213  lnmlmic  31238  gicabl  31251  suprnmpt  31654  fsumnncl  31775  ellimciota  31823  islpcn  31848  lptre2pt  31849  stoweidlem35  32020  fourierdlem31  32123  fourier2  32213  pfxcl  32503  mgmpropd  32725  opmpt2ismgm  32757  nzerooringczr  33024  alscn0d  33354  onfrALT  33464  onfrALTVD  33834  iunconlem2  33878  bnj521  33935  bnj1189  34208  bnj1279  34217  bj-n0i  34646  atex  35273  llnn0  35383  lplnn0N  35414  lvoln0N  35458  pmapglb2N  35638  pmapglb2xN  35639  elpaddn0  35667  osumcllem8N  35830  pexmidlem5N  35841  diaglbN  36925  diaintclN  36928  dibglbN  37036  dibintclN  37037  dihglblem2aN  37163  dihglblem5  37168  dihglbcpreN  37170  dihintcl  37214  xpcogend  37933  ndisj  37983