MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  n0 Structured version   Unicode version

Theorem n0 3639
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
StepHypRef Expression
1 nfcv 2574 . 2  |-  F/_ x A
21n0f 3638 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1551    e. wcel 1726    =/= wne 2601   (/)c0 3630
This theorem is referenced by:  neq0  3640  reximdva0  3641  n0moeu  3642  pssnel  3695  r19.2z  3719  r19.2zb  3720  r19.3rz  3721  r19.3rzv  3723  uniintsn  4089  iunn0  4153  trint0  4321  intex  4358  notzfaus  4376  nnullss  4427  exss  4428  opabn0  4487  wefrc  4578  wereu2  4581  onfr  4622  reusv2lem1  4726  reusv5OLD  4735  limuni3  4834  dmxp  5090  xpnz  5294  soex  5321  dmsnn0  5337  unixp0  5405  xpco  5416  eldmrexrnb  5879  isofrlem  6062  f1oweALT  6076  fo1stres  6372  fo2ndres  6373  ecdmn0  6949  map0g  7055  ixpn0  7096  resixpfo  7102  domdifsn  7193  xpdom3  7208  fodomr  7260  mapdom3  7281  findcard2  7350  unblem2  7362  marypha1lem  7440  brwdom2  7543  unxpwdom2  7558  ixpiunwdom  7561  zfreg  7565  zfreg2  7566  epfrs  7669  scott0  7812  cplem1  7815  fseqen  7910  finacn  7933  iunfictbso  7997  aceq2  8002  dfac3  8004  dfac9  8018  kmlem6  8037  kmlem8  8039  infpss  8099  fin23lem7  8198  enfin2i  8203  fin23lem21  8221  fin23lem31  8225  isf32lem9  8243  isf34lem4  8259  axdc2lem  8330  axdc3lem4  8335  ac6c4  8363  ac9  8365  ac6s4  8372  ac9s  8375  ttukeyg  8399  fpwwe2lem12  8518  wun0  8595  tsk0  8640  gruina  8695  genpn0  8882  prlem934  8912  ltaddpr  8913  ltexprlem1  8915  prlem936  8926  reclem2pr  8927  suplem1pr  8931  supsr  8989  axpre-sup  9046  infm3  9969  supmul1  9975  supmullem2  9977  supmul  9978  infmrcl  9989  negn0  10564  zsupss  10567  xrsupsslem  10887  xrinfmsslem  10888  supxrre  10908  infmxrre  10916  ixxub  10939  ixxlb  10940  ioorebas  11008  fzn0  11072  fzon0  11158  hashgt0elexb  11673  swrdcl  11768  maxprmfct  13115  4sqlem12  13326  vdwmc  13348  ramz  13395  ramub1  13398  mreiincl  13823  mremre  13831  mreexexlem4d  13874  iscatd2  13908  drsdirfi  14397  issubg2  14961  subgint  14966  giclcl  15061  gicrcl  15062  gicsym  15063  gictr  15064  gicen  15066  gicsubgen  15067  cntzssv  15129  sylow1lem4  15237  odcau  15240  sylow3  15269  cyggex2  15508  giccyg  15511  pgpfac1lem5  15639  subrgint  15892  lss0cl  16025  lmiclcl  16144  lmicrcl  16145  lmicsym  16146  lspsnat  16219  lspprat  16227  abvn0b  16364  cnsubrg  16761  cygzn  16853  toponmre  17159  iunconlem  17492  iuncon  17493  uncon  17494  clscon  17495  2ndcdisj  17521  2ndcsep  17524  1stcelcls  17526  txcls  17638  hmphsym  17816  hmphtr  17817  hmphen  17819  haushmphlem  17821  cmphmph  17822  conhmph  17823  reghmph  17827  nrmhmph  17828  hmphdis  17830  hmphen2  17833  fbdmn0  17868  isfbas2  17869  fbssint  17872  trfbas2  17877  filtop  17889  isfil2  17890  elfg  17905  fgcl  17912  filssufilg  17945  uffix2  17958  ufildom1  17960  hauspwpwf1  18021  hausflf2  18032  alexsubALTlem2  18081  ptcmplem2  18086  cnextf  18099  tgptsmscld  18182  ustfilxp  18244  xbln0  18446  lpbl  18535  met2ndci  18554  metustfbasOLD  18597  metustfbas  18598  restmetu  18619  reconn  18861  opnreen  18864  metdsre  18885  phtpcer  19022  phtpc01  19023  phtpcco2  19026  pcohtpy  19047  cfilfcls  19229  cmetcaulem  19243  cmetcau  19244  cmetss  19269  bcthlem5  19283  ovolicc2lem2  19416  ovolicc2lem5  19419  ioorcl2  19466  ioorinv2  19469  itg11  19585  dvlip  19879  dvne0  19897  mpfrcl  19941  fta1g  20092  plyssc  20121  fta1  20227  vieta1lem2  20230  umgraex  21360  eupath  21705  isgrp2d  21825  ubthlem1  22374  shintcli  22833  fmcncfil  24319  insiga  24522  pconcon  24920  txscon  24930  cvmsss2  24963  cvmopnlem  24967  cvmfolem  24968  cvmliftmolem2  24971  cvmlift2lem10  25001  cvmliftpht  25007  cvmlift3lem8  25015  dedekind  25189  dedekindle  25190  eldm3  25387  fundmpss  25392  elima4  25406  frmin  25519  nocvxmin  25648  axcontlem4  25908  axcontlem10  25914  supaddc  26239  supadd  26240  itg2addnclem2  26259  locfincmp  26386  comppfsc  26389  neibastop1  26390  neibastop2lem  26391  neibastop2  26392  fnemeet2  26398  fnejoin2  26400  neifg  26402  tailfb  26408  filnetlem3  26411  prdsbnd2  26506  heibor1lem  26520  bfp  26535  divrngidl  26640  rencldnfilem  26883  kelac1  27140  lnmlmic  27165  gicabl  27242  lmiclbs  27286  lmisfree  27291  symggen  27390  psgnunilem3  27398  stoweidlem35  27762  2spontn0vne  28407  frgrawopreglem2  28496  onfrALT  28697  onfrALTVD  29065  iunconlem2  29109  bnj521  29166  bnj1189  29440  bnj1279  29449  atex  30265  llnn0  30375  lplnn0N  30406  lvoln0N  30450  pmapglb2N  30630  pmapglb2xN  30631  elpaddn0  30659  osumcllem8N  30822  pexmidlem5N  30833  diaglbN  31915  diaintclN  31918  dibglbN  32026  dibintclN  32027  dihglblem2aN  32153  dihglblem5  32158  dihglbcpreN  32160  dihintcl  32204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-nul 3631
  Copyright terms: Public domain W3C validator