Theorem n0 3787

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

Syntax hints:   <-> wb 184   E.wex 1591   e. wcel 1762   =/= wne 2655   (/)c0 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-v 3108  df-dif 3472  df-nul 3779

This theorem is referenced by:  neq0  3788  reximdva0  3789  rspn0  3790  n0moeu  3791  pssnel  3885  r19.2z  3910  r19.2zb  3911  r19.3rz  3912  r19.3rzv  3914  uniintsn  4312  iunn0  4378  trint0  4550  intex  4596  notzfaus  4615  reusv2lem1  4641  reusv5OLD  4650  nnullss  4702  exss  4703  opabn0  4771  wefrc  4866  wereu2  4869  onfr  4910  dmxp  5212  xpnz  5417  dmsnn0  5464  unixp0  5532  xpco  5538  eldmrexrnb  6019  isofrlem  6215  limuni3  6658  soex  6717  f1oweALT  6758  fo1stres  6798  fo2ndres  6799  ecdmn0  7344  map0g  7448  ixpn0  7491  resixpfo  7497  domdifsn  7590  xpdom3  7605  fodomr  7658  mapdom3  7679  findcard2  7749  unblem2  7762  marypha1lem  7882  brwdom2  7988  unxpwdom2  8003  ixpiunwdom  8006  zfreg  8010  zfreg2  8011  epfrs  8151  scott0  8293  cplem1  8296  fseqen  8397  finacn  8420  iunfictbso  8484  aceq2  8489  dfac3  8491  dfac9  8505  kmlem6  8524  kmlem8  8526  infpss  8586  fin23lem7  8685  enfin2i  8690  fin23lem21  8708  fin23lem31  8712  isf32lem9  8730  isf34lem4  8746  axdc2lem  8817  axdc3lem4  8822  ac6c4  8850  ac9  8852  ac6s4  8859  ac9s  8862  ttukeyg  8886  fpwwe2lem12  9008  wun0  9085  tsk0  9130  gruina  9185  genpn0  9370  prlem934  9400  ltaddpr  9401  ltexprlem1  9403  prlem936  9414  reclem2pr  9415  suplem1pr  9419  supsr  9478  axpre-sup  9535  dedekind  9732  dedekindle  9733  infm3  10491  supmul1  10497  supmullem2  10499  supmul  10500  infmrcl  10511  negn0  11157  zsupss  11160  xrsupsslem  11487  xrinfmsslem  11488  supxrre  11508  infmxrre  11516  ixxub  11539  ixxlb  11540  ioorebas  11615  fzn0  11689  fzon0  11802  hashgt0elexb  12420  swrdcl  12596  maxprmfct  14102  4sqlem12  14322  vdwmc  14344  ramz  14391  ramub1  14394  mreiincl  14840  mremre  14848  mreexexlem4d  14891  iscatd2  14925  drsdirfi  15414  issubg2  16004  subgint  16013  giclcl  16108  gicrcl  16109  gicsym  16110  gictr  16111  gicen  16113  gicsubgen  16114  cntzssv  16154  symggen  16284  psgnunilem3  16310  sylow1lem4  16410  odcau  16413  sylow3  16442  cyggex2  16683  giccyg  16686  pgpfac1lem5  16913  brric2  17170  subrgint  17227  lss0cl  17369  lmiclcl  17492  lmicrcl  17493  lmicsym  17494  lspsnat  17567  lspprat  17575  abvn0b  17715  mpfrcl  17951  ply1frcl  18119  cnsubrg  18239  cygzn  18369  lmiclbs  18632  lmisfree  18637  lmictra  18640  mdetdiaglem  18860  mdet0  18868  toponmre  19353  iunconlem  19687  iuncon  19688  uncon  19689  clscon  19690  2ndcdisj  19716  2ndcsep  19719  1stcelcls  19721  txcls  19833  hmphsym  20011  hmphtr  20012  hmphen  20014  haushmphlem  20016  cmphmph  20017  conhmph  20018  reghmph  20022  nrmhmph  20023  hmphdis  20025  hmphen2  20028  fbdmn0  20063  isfbas2  20064  fbssint  20067  trfbas2  20072  filtop  20084  isfil2  20085  elfg  20100  fgcl  20107  filssufilg  20140  uffix2  20153  ufildom1  20155  hauspwpwf1  20216  hausflf2  20227  alexsubALTlem2  20276  ptcmplem2  20281  cnextf  20294  tgptsmscld  20381  ustfilxp  20443  xbln0  20645  lpbl  20734  met2ndci  20753  metustfbasOLD  20796  metustfbas  20797  restmetu  20818  reconn  21061  opnreen  21064  metdsre  21085  phtpcer  21223  phtpc01  21224  phtpcco2  21227  pcohtpy  21248  cfilfcls  21441  cmetcaulem  21455  cmetcau  21456  cmetss  21481  bcthlem5  21495  ovolicc2lem2  21657  ovolicc2lem5  21660  ioorcl2  21709  ioorinv2  21712  itg11  21826  dvlip  22122  dvne0  22140  fta1g  22296  plyssc  22325  fta1  22431  vieta1lem2  22434  axcontlem4  23939  axcontlem10  23945  umgraex  23986  wlk0  24423  2spontn0vne  24549  eupath  24643  isgrp2d  24763  ubthlem1  25312  shintcli  25773  fpwrelmapffslem  27077  fmcncfil  27399  insiga  27627  pconcon  28166  txscon  28176  cvmsss2  28209  cvmopnlem  28213  cvmfolem  28214  cvmliftmolem2  28217  cvmlift2lem10  28247  cvmliftpht  28253  cvmlift3lem8  28261  eldm3  28618  fundmpss  28623  elima4  28636  frmin  28749  nocvxmin  28878  supaddc  29468  supadd  29469  itg2addnclem2  29495  locfincmp  29627  comppfsc  29630  neibastop1  29631  neibastop2lem  29632  neibastop2  29633  fnemeet2  29639  fnejoin2  29641  neifg  29643  tailfb  29649  filnetlem3  29652  prdsbnd2  29745  heibor1lem  29759  bfp  29774  divrngidl  29879  rencldnfilem  30209  kelac1  30466  lnmlmic  30491  gicabl  30504  suprnmpt  30848  ellimciota  30975  islpcn  31000  lptre2pt  31001  stoweidlem35  31154  fourierdlem31  31257  fourier2  31347  usgn0fidegnn0  31748  frgrawopreglem2  31764  alscn0d  32166  onfrALT  32276  onfrALTVD  32646  iunconlem2  32690  bnj521  32747  bnj1189  33019  bnj1279  33028  bj-n0i  33459  atex  34077  llnn0  34187  lplnn0N  34218  lvoln0N  34262  pmapglb2N  34442  pmapglb2xN  34443  elpaddn0  34471  osumcllem8N  34634  pexmidlem5N  34645  diaglbN  35727  diaintclN  35730  dibglbN  35838  dibintclN  35839  dihglblem2aN  35965  dihglblem5  35970  dihglbcpreN  35972  dihintcl  36016  xpcogend  36658