Theorem n0 3641

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

Syntax hints:   <-> wb 184   E.wex 1586   e. wcel 1756   =/= wne 2601   (/)c0 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-nul 3633

This theorem is referenced by:  neq0  3642  reximdva0  3643  rspn0  3644  n0moeu  3645  pssnel  3739  r19.2z  3764  r19.2zb  3765  r19.3rz  3766  r19.3rzv  3768  uniintsn  4160  iunn0  4225  trint0  4397  intex  4443  notzfaus  4462  reusv2lem1  4488  reusv5OLD  4497  nnullss  4549  exss  4550  opabn0  4614  wefrc  4709  wereu2  4712  onfr  4753  dmxp  5053  xpnz  5252  dmsnn0  5299  unixp0  5366  xpco  5372  eldmrexrnb  5845  isofrlem  6026  limuni3  6458  soex  6516  f1oweALT  6556  fo1stres  6595  fo2ndres  6596  ecdmn0  7135  map0g  7244  ixpn0  7287  resixpfo  7293  domdifsn  7386  xpdom3  7401  fodomr  7454  mapdom3  7475  findcard2  7544  unblem2  7557  marypha1lem  7675  brwdom2  7780  unxpwdom2  7795  ixpiunwdom  7798  zfreg  7802  zfreg2  7803  epfrs  7943  scott0  8085  cplem1  8088  fseqen  8189  finacn  8212  iunfictbso  8276  aceq2  8281  dfac3  8283  dfac9  8297  kmlem6  8316  kmlem8  8318  infpss  8378  fin23lem7  8477  enfin2i  8482  fin23lem21  8500  fin23lem31  8504  isf32lem9  8522  isf34lem4  8538  axdc2lem  8609  axdc3lem4  8614  ac6c4  8642  ac9  8644  ac6s4  8651  ac9s  8654  ttukeyg  8678  fpwwe2lem12  8800  wun0  8877  tsk0  8922  gruina  8977  genpn0  9164  prlem934  9194  ltaddpr  9195  ltexprlem1  9197  prlem936  9208  reclem2pr  9209  suplem1pr  9213  supsr  9271  axpre-sup  9328  dedekind  9525  dedekindle  9526  infm3  10281  supmul1  10287  supmullem2  10289  supmul  10290  infmrcl  10301  negn0  10933  zsupss  10936  xrsupsslem  11261  xrinfmsslem  11262  supxrre  11282  infmxrre  11290  ixxub  11313  ixxlb  11314  ioorebas  11383  fzn0  11456  fzon0  11561  hashgt0elexb  12152  swrdcl  12307  maxprmfct  13791  4sqlem12  14009  vdwmc  14031  ramz  14078  ramub1  14081  mreiincl  14526  mremre  14534  mreexexlem4d  14577  iscatd2  14611  drsdirfi  15100  issubg2  15687  subgint  15696  giclcl  15791  gicrcl  15792  gicsym  15793  gictr  15794  gicen  15796  gicsubgen  15797  cntzssv  15837  symggen  15967  psgnunilem3  15993  sylow1lem4  16091  odcau  16094  sylow3  16123  cyggex2  16364  giccyg  16367  pgpfac1lem5  16570  subrgint  16867  lss0cl  17008  lmiclcl  17131  lmicrcl  17132  lmicsym  17133  lspsnat  17206  lspprat  17214  abvn0b  17354  mpfrcl  17584  ply1frcl  17733  cnsubrg  17853  cygzn  17983  lmiclbs  18246  lmisfree  18251  lmictra  18254  mdet1  18388  toponmre  18677  iunconlem  19011  iuncon  19012  uncon  19013  clscon  19014  2ndcdisj  19040  2ndcsep  19043  1stcelcls  19045  txcls  19157  hmphsym  19335  hmphtr  19336  hmphen  19338  haushmphlem  19340  cmphmph  19341  conhmph  19342  reghmph  19346  nrmhmph  19347  hmphdis  19349  hmphen2  19352  fbdmn0  19387  isfbas2  19388  fbssint  19391  trfbas2  19396  filtop  19408  isfil2  19409  elfg  19424  fgcl  19431  filssufilg  19464  uffix2  19477  ufildom1  19479  hauspwpwf1  19540  hausflf2  19551  alexsubALTlem2  19600  ptcmplem2  19605  cnextf  19618  tgptsmscld  19705  ustfilxp  19767  xbln0  19969  lpbl  20058  met2ndci  20077  metustfbasOLD  20120  metustfbas  20121  restmetu  20142  reconn  20385  opnreen  20388  metdsre  20409  phtpcer  20547  phtpc01  20548  phtpcco2  20551  pcohtpy  20572  cfilfcls  20765  cmetcaulem  20779  cmetcau  20780  cmetss  20805  bcthlem5  20819  ovolicc2lem2  20981  ovolicc2lem5  20984  ioorcl2  21032  ioorinv2  21035  itg11  21149  dvlip  21445  dvne0  21463  fta1g  21619  plyssc  21648  fta1  21754  vieta1lem2  21757  axcontlem4  23181  axcontlem10  23187  umgraex  23225  eupath  23570  isgrp2d  23690  ubthlem1  24239  shintcli  24700  fpwrelmapffslem  26000  fmcncfil  26330  insiga  26549  pconcon  27089  txscon  27099  cvmsss2  27132  cvmopnlem  27136  cvmfolem  27137  cvmliftmolem2  27140  cvmlift2lem10  27170  cvmliftpht  27176  cvmlift3lem8  27184  eldm3  27541  fundmpss  27546  elima4  27559  frmin  27672  nocvxmin  27801  supaddc  28388  supadd  28389  itg2addnclem2  28415  locfincmp  28547  comppfsc  28550  neibastop1  28551  neibastop2lem  28552  neibastop2  28553  fnemeet2  28559  fnejoin2  28561  neifg  28563  tailfb  28569  filnetlem3  28572  prdsbnd2  28665  heibor1lem  28679  bfp  28694  divrngidl  28799  rencldnfilem  29130  kelac1  29387  lnmlmic  29412  gicabl  29425  stoweidlem35  29801  wlk0  30263  2spontn0vne  30377  usgn0fidegnn0  30593  frgrawopreglem2  30609  mdet0  30864  mdetdiaglem  30866  alscn0d  31076  onfrALT  31186  onfrALTVD  31556  iunconlem2  31600  bnj521  31657  bnj1189  31929  bnj1279  31938  bj-n0i  32338  atex  32943  llnn0  33053  lplnn0N  33084  lvoln0N  33128  pmapglb2N  33308  pmapglb2xN  33309  elpaddn0  33337  osumcllem8N  33500  pexmidlem5N  33511  diaglbN  34593  diaintclN  34596  dibglbN  34704  dibintclN  34705  dihglblem2aN  34831  dihglblem5  34836  dihglbcpreN  34838  dihintcl  34882