Theorem n0 3931

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

Syntax hints:   <-> wb 196   E.wex 1704   e. wcel 1990   =/= wne 2794   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  reximdva0  3933  rspn0  3934  n0rex  3935  n0moeu  3937  eqeuel  3941  pssnel  4039  r19.2z  4060  r19.2zb  4061  r19.3rz  4062  uniintsn  4514  iunn0  4580  trintss  4769  intex  4820  notzfaus  4840  reusv2lem1  4868  nnullss  4930  exss  4931  opabn0  5006  wefrc  5108  wereu2  5111  dmxp  5344  xpnz  5553  dmsnn0  5600  unixp0  5669  xpco  5675  onfr  5763  fveqdmss  6354  eldmrexrnb  6366  isofrlem  6590  limuni3  7052  soex  7109  f1oweALT  7152  fo1stres  7192  fo2ndres  7193  ecdmn0  7789  map0g  7897  ixpn0  7940  resixpfo  7946  domdifsn  8043  xpdom3  8058  fodomr  8111  mapdom3  8132  findcard2  8200  unblem2  8213  marypha1lem  8339  brwdom2  8478  unxpwdom2  8493  ixpiunwdom  8496  zfreg  8500  zfregOLD  8502  zfreg2OLD  8503  epfrs  8607  scott0  8749  cplem1  8752  fseqen  8850  finacn  8873  iunfictbso  8937  aceq2  8942  dfac3  8944  dfac9  8958  kmlem6  8977  kmlem8  8979  infpss  9039  fin23lem7  9138  enfin2i  9143  fin23lem21  9161  fin23lem31  9165  isf32lem9  9183  isf34lem4  9199  axdc2lem  9270  axdc3lem4  9275  ac6c4  9303  ac9  9305  ac6s4  9312  ac9s  9315  ttukeyg  9339  fpwwe2lem12  9463  wun0  9540  tsk0  9585  gruina  9640  genpn0  9825  prlem934  9855  ltaddpr  9856  ltexprlem1  9858  prlem936  9869  reclem2pr  9870  suplem1pr  9874  supsr  9933  axpre-sup  9990  dedekind  10200  dedekindle  10201  negn0  10459  infm3  10982  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  supmul  10995  zsupss  11777  xrsupsslem  12137  xrinfmsslem  12138  supxrre  12157  infxrre  12166  ixxub  12196  ixxlb  12197  ioorebas  12275  fzn0  12355  fzon0  12487  hashgt0elexb  13190  swrdcl  13419  xpcogend  13713  maxprmfct  15421  4sqlem12  15660  vdwmc  15682  ramz  15729  ramub1  15732  mreiincl  16256  mremre  16264  mreexexlem4d  16307  iscatd2  16342  cic  16459  drsdirfi  16938  opifismgm  17258  dfgrp3lem  17513  dfgrp3e  17515  issubg2  17609  subgint  17618  giclcl  17714  gicrcl  17715  gicsym  17716  gictr  17717  gicen  17720  gicsubgen  17721  cntzssv  17761  symggen  17890  psgnunilem3  17916  sylow1lem4  18016  odcau  18019  sylow3  18048  cyggex2  18298  giccyg  18301  pgpfac1lem5  18478  brric2  18745  subrgint  18802  lss0cl  18947  lmiclcl  19070  lmicrcl  19071  lmicsym  19072  lspsnat  19145  lspprat  19153  abvn0b  19302  mpfrcl  19518  ply1frcl  19683  cnsubrg  19806  cygzn  19919  lmiclbs  20176  lmisfree  20181  lmictra  20184  mdetdiaglem  20404  mdet0  20412  toponmre  20897  iunconnlem  21230  iunconn  21231  unconn  21232  clsconn  21233  2ndcdisj  21259  2ndcsep  21262  1stcelcls  21264  locfincmp  21329  comppfsc  21335  txcls  21407  hmphsym  21585  hmphtr  21586  hmphen  21588  haushmphlem  21590  cmphmph  21591  connhmph  21592  reghmph  21596  nrmhmph  21597  hmphdis  21599  hmphen2  21602  fbdmn0  21638  isfbas2  21639  fbssint  21642  trfbas2  21647  filtop  21659  isfil2  21660  elfg  21675  fgcl  21682  filssufilg  21715  uffix2  21728  ufildom1  21730  hauspwpwf1  21791  hausflf2  21802  alexsubALTlem2  21852  ptcmplem2  21857  cnextf  21870  tgptsmscld  21954  ustfilxp  22016  xbln0  22219  lpbl  22308  met2ndci  22327  metustfbas  22362  restmetu  22375  reconn  22631  opnreen  22634  metdsre  22656  phtpcer  22794  phtpcerOLD  22795  phtpc01  22796  phtpcco2  22799  pcohtpy  22820  cfilfcls  23072  cmetcaulem  23086  cmetcau  23087  cmetss  23113  bcthlem5  23125  ovolicc2lem2  23286  ovolicc2lem5  23289  ioorcl2  23340  ioorinv2  23343  itg11  23458  dvlip  23756  dvne0  23774  fta1g  23927  plyssc  23956  fta1  24063  vieta1lem2  24066  hpgerlem  25657  axcontlem4  25847  axcontlem10  25853  upgrex  25987  fusgrn0degnn0  26395  uhgrvd00  26430  wspthsnonn0vne  26813  eulerpath  27101  frgrwopreglem2  27177  ubthlem1  27726  shintcli  28188  fpwrelmapffslem  29507  fmcncfil  29977  insiga  30200  unelldsys  30221  bnj521  30805  bnj1189  31077  bnj1279  31086  pconnconn  31213  txsconn  31223  cvmsss2  31256  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmlift2lem10  31294  cvmliftpht  31300  cvmlift3lem8  31308  eldm3  31651  fundmpss  31664  elima4  31679  frmin  31739  nocvxmin  31894  sslttr  31914  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  fnemeet2  32362  fnejoin2  32364  neifg  32366  tailfb  32372  filnetlem3  32375  bj-n0i  32935  bj-rest10  33041  bj-restn0  33043  poimirlem30  33439  itg2addnclem2  33462  prdsbnd2  33594  heibor1lem  33608  bfp  33623  divrngidl  33827  atex  34692  llnn0  34802  lplnn0N  34833  lvoln0N  34877  pmapglb2N  35057  pmapglb2xN  35058  elpaddn0  35086  osumcllem8N  35249  pexmidlem5N  35260  diaglbN  36344  diaintclN  36347  dibglbN  36455  dibintclN  36456  dihglblem2aN  36582  dihglblem5  36587  dihglbcpreN  36589  dihintcl  36633  rencldnfilem  37384  kelac1  37633  lnmlmic  37658  gicabl  37669  ndisj  38063  neik0pk1imk0  38345  ntrneineine0lem  38381  onfrALT  38764  onfrALTVD  39127  iunconnlem2  39171  snelmap  39254  eliin2f  39287  suprnmpt  39355  disjinfi  39380  mapss2  39397  difmap  39399  infrpge  39567  infxrlesupxr  39663  inficc  39761  fsumnncl  39803  ellimciota  39846  islpcn  39871  lptre2pt  39872  stoweidlem35  40252  fourierdlem31  40355  fourier2  40444  qndenserrnbllem  40514  qndenserrnopn  40518  qndenserrn  40519  intsaluni  40547  sge0cl  40598  ovn0lem  40779  ovnsubaddlem2  40785  hoidmvval0b  40804  hspdifhsp  40830  pfxcl  41386  mgmpropd  41775  opmpt2ismgm  41807  nzerooringczr  42072  alscn0d  42541