Theorem n0 3776

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

Syntax hints:   <-> wb 184   E.wex 1597   e. wcel 1802   =/= wne 2636   (/)c0 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-v 3095  df-dif 3461  df-nul 3768

This theorem is referenced by:  neq0  3777  reximdva0  3778  rspn0  3779  n0moeu  3780  pssnel  3875  r19.2z  3900  r19.2zb  3901  r19.3rz  3902  r19.3rzv  3904  uniintsn  4305  iunn0  4371  trint0  4543  intex  4589  notzfaus  4608  reusv2lem1  4634  reusv5OLD  4643  nnullss  4695  exss  4696  opabn0  4764  wefrc  4859  wereu2  4862  onfr  4903  dmxp  5207  xpnz  5412  dmsnn0  5459  unixp0  5527  xpco  5533  fveqdmss  6007  eldmrexrnb  6019  isofrlem  6217  limuni3  6668  soex  6724  f1oweALT  6765  fo1stres  6805  fo2ndres  6806  ecdmn0  7352  map0g  7456  ixpn0  7499  resixpfo  7505  domdifsn  7598  xpdom3  7613  fodomr  7666  mapdom3  7687  findcard2  7758  unblem2  7771  marypha1lem  7891  brwdom2  7997  unxpwdom2  8012  ixpiunwdom  8015  zfreg  8019  zfreg2  8020  epfrs  8160  scott0  8302  cplem1  8305  fseqen  8406  finacn  8429  iunfictbso  8493  aceq2  8498  dfac3  8500  dfac9  8514  kmlem6  8533  kmlem8  8535  infpss  8595  fin23lem7  8694  enfin2i  8699  fin23lem21  8717  fin23lem31  8721  isf32lem9  8739  isf34lem4  8755  axdc2lem  8826  axdc3lem4  8831  ac6c4  8859  ac9  8861  ac6s4  8868  ac9s  8871  ttukeyg  8895  fpwwe2lem12  9017  wun0  9094  tsk0  9139  gruina  9194  genpn0  9379  prlem934  9409  ltaddpr  9410  ltexprlem1  9412  prlem936  9423  reclem2pr  9424  suplem1pr  9428  supsr  9487  axpre-sup  9544  dedekind  9742  dedekindle  9743  infm3  10503  supmul1  10509  supmullem2  10511  supmul  10512  infmrcl  10523  negn0  11172  zsupss  11175  xrsupsslem  11502  xrinfmsslem  11503  supxrre  11523  infmxrre  11531  ixxub  11554  ixxlb  11555  ioorebas  11630  fzn0  11704  fzon0  11819  hashgt0elexb  12441  swrdcl  12620  maxprmfct  14126  4sqlem12  14346  vdwmc  14368  ramz  14415  ramub1  14418  mreiincl  14865  mremre  14873  mreexexlem4d  14916  iscatd2  14950  drsdirfi  15436  opifismgm  15754  issubg2  16085  subgint  16094  giclcl  16189  gicrcl  16190  gicsym  16191  gictr  16192  gicen  16194  gicsubgen  16195  cntzssv  16235  symggen  16364  psgnunilem3  16390  sylow1lem4  16490  odcau  16493  sylow3  16522  cyggex2  16768  giccyg  16771  pgpfac1lem5  16998  brric2  17262  subrgint  17319  lss0cl  17461  lmiclcl  17584  lmicrcl  17585  lmicsym  17586  lspsnat  17659  lspprat  17667  abvn0b  17819  mpfrcl  18055  ply1frcl  18223  cnsubrg  18346  cygzn  18476  lmiclbs  18739  lmisfree  18744  lmictra  18747  mdetdiaglem  18967  mdet0  18975  toponmre  19460  iunconlem  19794  iuncon  19795  uncon  19796  clscon  19797  2ndcdisj  19823  2ndcsep  19826  1stcelcls  19828  locfincmp  19893  comppfsc  19899  txcls  19971  hmphsym  20149  hmphtr  20150  hmphen  20152  haushmphlem  20154  cmphmph  20155  conhmph  20156  reghmph  20160  nrmhmph  20161  hmphdis  20163  hmphen2  20166  fbdmn0  20201  isfbas2  20202  fbssint  20205  trfbas2  20210  filtop  20222  isfil2  20223  elfg  20238  fgcl  20245  filssufilg  20278  uffix2  20291  ufildom1  20293  hauspwpwf1  20354  hausflf2  20365  alexsubALTlem2  20414  ptcmplem2  20419  cnextf  20432  tgptsmscld  20519  ustfilxp  20581  xbln0  20783  lpbl  20872  met2ndci  20891  metustfbasOLD  20934  metustfbas  20935  restmetu  20956  reconn  21199  opnreen  21202  metdsre  21223  phtpcer  21361  phtpc01  21362  phtpcco2  21365  pcohtpy  21386  cfilfcls  21579  cmetcaulem  21593  cmetcau  21594  cmetss  21619  bcthlem5  21633  ovolicc2lem2  21795  ovolicc2lem5  21798  ioorcl2  21847  ioorinv2  21850  itg11  21964  dvlip  22260  dvne0  22278  fta1g  22434  plyssc  22463  fta1  22569  vieta1lem2  22572  hpgerlem  23999  axcontlem4  24135  axcontlem10  24141  umgraex  24188  2spontn0vne  24752  eupath  24846  usgn0fidegnn0  24894  frgrawopreglem2  24910  isgrp2d  25102  ubthlem1  25651  shintcli  26112  fpwrelmapffslem  27420  fmcncfil  27779  insiga  28003  pconcon  28542  txscon  28552  cvmsss2  28585  cvmopnlem  28589  cvmfolem  28590  cvmliftmolem2  28593  cvmlift2lem10  28623  cvmliftpht  28629  cvmlift3lem8  28637  eldm3  29159  fundmpss  29164  elima4  29177  frmin  29290  nocvxmin  29419  supaddc  30009  supadd  30010  itg2addnclem2  30035  neibastop1  30145  neibastop2lem  30146  neibastop2  30147  fnemeet2  30153  fnejoin2  30155  neifg  30157  tailfb  30163  filnetlem3  30166  prdsbnd2  30259  heibor1lem  30273  bfp  30288  divrngidl  30393  rencldnfilem  30722  kelac1  30977  lnmlmic  31002  gicabl  31015  suprnmpt  31397  ellimciota  31524  islpcn  31549  lptre2pt  31550  stoweidlem35  31702  fourierdlem31  31805  fourier2  31895  mgmpropd  32297  opmpt2ismgm  32328  alscn0d  32920  onfrALT  33029  onfrALTVD  33399  iunconlem2  33443  bnj521  33500  bnj1189  33772  bnj1279  33781  bj-n0i  34215  atex  34832  llnn0  34942  lplnn0N  34973  lvoln0N  35017  pmapglb2N  35197  pmapglb2xN  35198  elpaddn0  35226  osumcllem8N  35389  pexmidlem5N  35400  diaglbN  36484  diaintclN  36487  dibglbN  36595  dibintclN  36596  dihglblem2aN  36722  dihglblem5  36727  dihglbcpreN  36729  dihintcl  36773  xpcogend  37428