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

Theorem vex 3059
Description: All setvar variables are sets (see isset 3060). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
vex  |-  x  e. 
_V

Proof of Theorem vex
StepHypRef Expression
1 equid 1865 . 2  |-  x  =  x
2 df-v 3058 . . 3  |-  _V  =  { x  |  x  =  x }
32abeq2i 2573 . 2  |-  ( x  e.  _V  <->  x  =  x )
41, 3mpbir 214 1  |-  x  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1897   _Vcvv 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058
This theorem is referenced by:  isset  3060  eqvisset  3064  ralv  3072  rexv  3073  reuv  3074  rmov  3075  rabab  3076  sbhypf  3106  ralab  3210  rexab  3212  moeq3  3226  reu8  3245  sbc2or  3287  csbiebg  3397  ddif  3576  dfun2  3689  dfin2  3690  vn0  3750  eqv  3759  abvor0  3761  sbcnestgf  3795  csbvarg  3803  sbnfc2  3807  csbun  3809  csbin  3810  sbss  3890  csbif  3942  ifexg  3961  selpw  3969  ssnid  4008  dftp2  4029  prnzg  4104  snssg  4117  difprsnss  4119  sneqrg  4153  preq12bg  4167  prel12g  4168  pwpr  4207  pwtp  4208  pwv  4210  unipr  4224  uniprg  4225  unisng  4227  elintg  4255  elintrabg  4260  intss1  4262  ssint  4263  intmin  4267  intssOLD  4269  intssuni  4270  intmin4  4277  intab  4278  intun  4280  intpr  4281  intprg  4282  uniintsn  4285  iinconst  4301  iuniin  4302  iinss1  4304  dfiin2g  4324  dfiunv2  4327  ssiinf  4340  iinss  4342  iinss2  4343  0iin  4349  iinab  4352  iinun2  4357  iundif2  4358  iindif2  4360  iinin2  4361  iinuni  4378  iinpw  4383  brab1  4461  mptv  4509  trint  4525  trintss  4526  vprc  4554  inex1g  4559  ssexg  4562  intex  4572  inuni  4578  axpweq  4593  pwexg  4600  eusvnf  4611  axpr  4651  zfpair2  4653  elALT  4656  sspwb  4662  nnullss  4675  exss  4676  opth  4689  opthg  4690  copsexg  4700  copsex4g  4703  moop2  4709  euotd  4715  opelopabsbALT  4723  opelopabsb  4724  csbopab  4746  csbopabgALT  4747  pwssun  4758  epelg  4764  epel  4766  dfid3  4768  dfid4  4769  pofun  4789  epse  4835  wefrc  4846  0nelxp  4880  opelxp  4882  opeliunxp  4904  elvv  4911  elvvv  4912  elvvuni  4913  xpsspw  4966  relopabi  4977  opabid2  4982  difopab  4984  xpiindi  4988  ralxpf  4999  relop  5003  cnvco  5038  dfrn2  5041  dfdm4  5045  dmss  5052  dmin  5060  dmiun  5061  dmuni  5062  dm0  5066  dmi  5067  reldm0  5070  elreldm  5077  elrnmpt1  5101  dmrnssfld  5111  dmcoss  5112  dmcosseq  5114  opelresg  5130  resieq  5133  dmres  5143  elres  5158  relssres  5160  resopab  5169  iss  5170  dfres2  5175  restidsing  5179  dfima2  5188  imadmrn  5196  imai  5198  csbima12  5203  csbima12gOLD  5204  elimasng  5212  args  5214  epini  5216  iniseg  5217  inisegn0  5218  dffr3  5219  dfse2  5220  cotrg  5229  issref  5231  cnvsym  5232  intasym  5233  asymref  5234  asymref2  5235  intirr  5236  brcodir  5237  codir  5238  qfto  5239  poirr2  5242  cnvopab  5255  cnv0  5257  cnvi  5258  cnvdif  5260  rniun  5264  dminss  5268  imainss  5269  inimasn  5271  xpdifid  5283  ssrnres  5293  rninxp  5294  dminxp  5295  cnvcnv3  5303  dfrel2  5304  dmsnn0  5319  dmsnopg  5325  cnvcnvsn  5331  dmsnsnsn  5332  cnvsng  5340  cnvresima  5342  dfco2  5352  dfco2a  5353  cores  5356  resco  5357  imaco  5358  rnco  5359  coiun  5363  co02  5367  coi1  5369  coass  5372  relssdmrn  5374  unielrel  5378  unixp0  5388  ressn  5390  cnviin  5391  cnvpo  5392  cnvso  5393  dfpred3g  5409  predpo  5416  predbrg  5418  setlikespec  5419  predep  5424  preddowncl  5425  tz6.26  5429  tron  5464  onfr  5480  sucel  5514  suctr  5524  uniabio  5574  iotaval  5575  sniota  5591  csbiota  5593  dffun2  5610  dffun7  5626  dffun8  5627  dffun9  5628  funopg  5632  funssres  5640  funun  5642  funcnvsn  5645  funcnv2  5663  funcnv  5664  funcnv3  5665  fun2cnv  5666  imadif  5679  isarep1  5683  2elresin  5708  fnres  5713  fcnvres  5782  fconstg  5792  f1osng  5875  dffv3  5883  fv3  5900  fvres  5901  nfunsn  5918  funimass4  5938  opabiotafun  5948  opabiota  5950  ssimaexg  5953  dffv2  5960  dmfco  5961  fvopab6  5997  fndmdif  6008  iinpreima  6032  fvn0ssdmfun  6035  fvelrn  6037  dff3  6057  dffo4  6060  exfo  6062  f1ompt  6066  fmptco  6079  fsng  6086  fsn2g  6087  dfmpt  6092  fnressn  6099  fressnfv  6101  fvsng  6121  tpres  6140  fnprb  6146  fntpb  6147  fnpr2g  6148  funfvima3  6166  idref  6170  fvclss  6171  abrexco  6173  imaiun  6174  dff13  6183  fsnex  6205  foeqcnvco  6222  f1eqcocnv  6223  fliftcnv  6228  isocnv2  6246  isomin  6252  isoini  6253  isofr  6257  isose  6258  knatar  6272  riotav  6281  csbriota  6288  oprabid  6341  csbov123  6348  0neqopab  6360  oprabv  6365  eloprabga  6409  mpt2v  6412  caovmo  6532  f1opw  6549  porpss  6601  sorpss  6602  uniexg  6614  unexb  6617  snnex  6623  uniuni  6626  onint  6648  unon  6684  ordunisuc  6685  onuninsuci  6693  orduninsuc  6696  limsssuc  6703  limuni3  6705  tfinds  6712  tfindsg  6713  tfindsg2  6714  tfinds2  6716  dfom2  6720  peano5  6742  finds  6745  findsg  6746  finds2  6747  resiexg  6755  exse2  6758  elxp4  6763  elxp5  6764  f1oexbi  6769  funcnvuni  6772  fun11iun  6779  zfrep6  6787  fvresex  6792  opabex3d  6797  opabex3  6798  f1oweALT  6803  wemoiso  6804  wemoiso2  6805  ofmres  6815  op1stg  6831  op2ndg  6832  1stval2  6836  2ndval2  6837  fo1st  6839  fo2nd  6840  f1stres  6841  f2ndres  6842  fo1stres  6843  fo2ndres  6844  1st2val  6845  2nd2val  6846  xp1st  6849  xp2nd  6850  sbcopeq1a  6871  csbopeq1a  6872  opiota  6878  eloprabi  6881  mpt2mptsx  6882  dmmpt2ssx  6884  fmpt2x  6885  ovmptss  6903  fmpt2co  6905  df1st2  6908  df2nd2  6909  1stconst  6910  2ndconst  6911  curry1  6914  curry2  6917  fparlem1  6922  fparlem2  6923  fpar  6926  fsplit  6927  fo2ndf  6929  f1o2ndf1  6930  frxp  6932  xporderlem  6933  soxp  6935  fnwelem  6937  fnse  6939  suppvalbr  6944  cnvimadfsn  6949  suppimacnv  6951  reldmtpos  7006  dmtpos  7010  rntpos  7011  ovtpos  7013  dftpos3  7016  dftpos4  7017  tpostpos  7018  wfrlem5  7065  wfrlem10  7070  wfrlem12  7072  wfrlem13  7073  wfrlem17  7077  onovuni  7086  smogt  7111  dfrecs3  7116  tfrlem3  7121  tfrlem5  7123  tfrlem8  7127  tfrlem9a  7129  tfrlem16  7136  tz7.44lem1  7148  rdg0g  7170  rdglim2  7175  tz7.48-1  7185  seqomlem1  7192  seqomlem2  7193  oacl  7262  omcl  7263  oecl  7264  oa0r  7265  om0r  7266  om1r  7269  oe1m  7271  oaordi  7272  oawordri  7276  oawordeulem  7280  oalimcl  7286  oaass  7287  oarec  7288  omordi  7292  omwordri  7298  omlimcl  7304  odi  7305  omass  7306  omeulem1  7308  oen0  7312  oeordi  7313  oewordri  7318  oeworde  7319  oeoalem  7322  oeoelem  7324  nnawordex  7363  omabs  7373  omsmolem  7379  ercnv  7409  iserd  7414  eqerlem  7420  eqer  7421  ecdmn0  7431  erth  7433  erdisj  7436  qsss  7449  ecid  7453  qsid  7454  iiner  7460  qsel  7467  erovlem  7484  ecopovsym  7490  ecopovtrn  7491  ecopover  7492  mapprc  7501  fnmap  7504  fnpm  7505  mapval2  7526  mapsn  7538  mapsncnv  7543  ralxpmap  7546  ixpconstg  7556  ixpprc  7568  ixpin  7572  ixpiin  7573  resixpfo  7585  elixpsn  7586  ixpsnf1o  7587  boxriin  7589  boxcutc  7590  bren  7603  brdomg  7604  domen  7607  domeng  7608  ctex  7609  idssen  7639  ener  7641  domtr  7647  ensn1g  7659  en1  7661  en1b  7662  fundmen  7668  fundmeng  7669  mapsnen  7672  unen  7677  domdifsn  7680  xpsnen  7681  xpsneng  7682  xpcomeng  7689  xpassen  7691  xpdom2  7692  xpdom2g  7693  domunsncan  7697  omxpenlem  7698  pw2f1o  7702  enfixsn  7706  sbthlem10  7716  sbth  7717  sbthcl  7719  domunsn  7747  fodomr  7748  pwdom  7749  canth2  7750  canth2g  7751  domssex  7758  xpf1o  7759  mapen  7761  mapunen  7766  map2xp  7767  mapdom2  7768  mapdom3  7769  ssenen  7771  infensuc  7775  nneneq  7780  php  7781  php2  7782  php3  7783  sucdom2  7793  1sdom  7800  unxpdomlem2  7802  unxpdomlem3  7803  isinf  7810  fineqv  7812  pssnn  7815  ssfi  7817  dif1en  7829  findcard  7835  findcard2  7836  findcard2s  7837  ac6sfi  7840  frfi  7841  fimax2g  7842  unbnn2  7853  isfinite2  7854  xpfi  7867  domunfican  7869  fiint  7873  fodomfi  7875  fodomfib  7876  iunfi  7887  pwfilem  7893  ixpfi2  7897  fissuni  7904  fipreima  7905  finsschain  7906  ssfii  7958  fi0  7959  fiin  7961  dffi2  7962  fipwuni  7965  fisn  7966  elfiun  7969  dffi3  7970  fifo  7971  marypha1lem  7972  dfsup2  7983  eqinf  8025  infval  8027  infcllem  8028  infglb  8031  infglbb  8032  ordiso2  8055  oismo  8080  hartogslem1  8082  hartogs  8084  wofib  8085  wemappo  8089  wemapsolem  8090  card2on  8094  brwdom  8107  brwdomn0  8109  brwdom2  8113  wdomtr  8115  wdompwdom  8118  canthwdom  8119  xpwdomg  8125  unxpwdom2  8128  ixpiunwdom  8131  zfregfr  8142  inf0  8151  inf3lema  8154  inf3lemd  8157  inf3lem1  8158  inf3lem2  8159  inf3lem3  8160  inf3lem5  8162  inf3lem6  8163  inf3lem7  8164  inf3  8165  infeq5  8167  omex  8173  dfom3  8177  dfom5  8180  infdifsn  8187  cantnfval2  8199  cantnflt  8202  oemapso  8212  cantnflem1  8219  wemapwe  8227  cnfcom  8230  cnfcom3clem  8235  epfrs  8240  tcvalg  8247  tctr  8249  tcmin  8250  r1sdom  8270  r1val1  8282  tz9.12lem3  8285  tz9.13  8287  tz9.13g  8288  rankf  8290  unir1  8309  rankvalg  8313  rankonidlem  8324  r1val2  8333  bndrank  8337  ranklim  8340  r1pwALT  8342  rankunb  8346  rankuni2b  8349  rankuni  8359  rankval4  8363  rankxplim  8375  rankxplim3  8377  rankxpsuc  8378  tcrank  8380  cp  8387  bnd2  8389  kardex  8390  karden  8391  cardf2  8402  tskwe  8409  cardlim  8431  harcard  8437  cardiun  8441  pm54.43  8459  r0weon  8468  infxpenlem  8469  infxpenc2lem2  8476  fseqenlem1  8480  fseqenlem2  8481  fseqen  8483  dfac8alem  8485  dfac8clem  8488  ac10ct  8490  ween  8491  acnlem  8504  finacn  8506  acndom  8507  acndom2  8510  wdomfil  8517  infpwfien  8518  alephon  8525  alephcard  8526  alephordi  8530  cardaleph  8545  alephval3  8566  iunfictbso  8570  aceq3lem  8576  dfac3  8577  dfac4  8578  dfac5lem1  8579  dfac5lem2  8580  dfac5lem3  8581  dfac5lem4  8582  dfac5lem5  8583  dfac5  8584  dfac2a  8585  dfac2  8586  dfac8  8590  dfac9  8591  dfac10b  8594  acacni  8595  dfacacn  8596  dfac13  8597  kmlem1  8605  kmlem2  8606  kmlem9  8613  kmlem10  8614  kmlem11  8615  kmlem12  8616  kmlem13  8617  cdafn  8624  pwsdompw  8659  infmap2  8673  ackbij1lem5  8679  ackbij1lem8  8682  ackbij2  8698  cflm  8705  cardcf  8707  cfeq0  8711  cfsuc  8712  cff1  8713  cfflb  8714  cflim2  8718  cfss  8720  cfslb2n  8723  cofsmo  8724  cfsmolem  8725  cfcoflem  8727  coftr  8728  sornom  8732  infpssr  8763  fin4en1  8764  enfin2i  8776  fin23lem26  8780  fin23lem14  8788  fin23lem16  8790  fin23lem17  8793  fin23lem21  8794  fin23lem32  8799  fin23lem34  8801  fin23lem39  8805  compssiso  8829  isf34lem4  8832  enfin1ai  8839  isfin1-3  8841  fin67  8850  dffin7-2  8853  fin1a2lem7  8861  fin1a2lem10  8864  fin1a2lem12  8866  fin1a2lem13  8867  fin12  8868  itunitc1  8875  itunitc  8876  ituniiun  8877  hsmexlem2  8882  hsmexlem4  8884  hsmex  8887  axcc2lem  8891  axcc3  8893  acncc  8895  fin41  8899  dominf  8900  dcomex  8902  axdc2lem  8903  axdc3lem2  8906  axdc3lem4  8908  axdc4lem  8910  axcclem  8912  ac9  8938  ac6s  8939  ac6sg  8943  ac9s  8948  numthcor  8949  zorn2lem1  8951  zorn2lem4  8954  zorn2lem7  8957  zorng  8959  zornn0g  8960  ttukeylem5  8968  ttukeylem6  8969  ttukeylem7  8970  axdclem  8974  axdclem2  8975  fodomg  8978  fodomb  8979  brdom3  8981  brdom5  8982  brdom4  8983  brdom7disj  8984  brdom6disj  8985  iunfo  8989  ondomon  9013  cardmin  9014  alephval2  9022  dominfac  9023  fpwwe2lem8  9087  fpwwe2lem11  9090  fpwwe2lem12  9091  fpwwe2lem13  9092  fpwwe2  9093  fpwwe  9096  canthwe  9101  canthp1lem1  9102  pwfseqlem1  9108  pwfseqlem2  9109  pwfseqlem3  9110  pwfseqlem4a  9111  pwfseqlem5  9113  pwxpndom2  9115  gch2  9125  gchac  9131  inawinalem  9139  winainflem  9143  winalim2  9146  winafp  9147  gchina  9149  wunfi  9171  intwun  9185  wunex2  9188  uniwun  9190  eltsk2g  9201  inttsk  9224  inar1  9225  rankcf  9227  tskcard  9231  tskuni  9233  gruun  9256  intgru  9264  ingru  9265  wfgru  9266  grudomon  9267  gruina  9268  grur1a  9269  grur1  9270  grutsk  9272  axgroth2  9275  grothpw  9276  grothpwex  9277  axgroth6  9278  grothomex  9279  grothac  9280  axgroth3  9281  grothprim  9284  grothtsk  9285  inaprc  9286  nqereu  9379  nqerf  9380  dmrecnq  9418  ltaddnq  9424  genpnnp  9455  genpnmax  9457  genpcl  9458  nqpr  9464  addclprlem1  9466  mulclprlem  9469  distrlem4pr  9476  1idpr  9479  prlem934  9483  ltaddpr  9484  ltexprlem3  9488  ltexprlem4  9489  ltexprlem6  9491  ltexprlem7  9492  prlem936  9497  reclem2pr  9498  reclem3pr  9499  mulasssr  9539  ltsosr  9543  0idsr  9546  1idsr  9547  ltasr  9549  recexsrlem  9552  mulgt0sr  9554  supsrlem  9560  ltresr  9589  axmulass  9606  axrrecex  9612  axpre-lttri  9614  wloglei  10173  lbinf  10586  lbinfmOLD  10587  supaddc  10601  supadd  10602  supmul1  10603  supmullem1  10604  supmullem2  10605  supmul  10606  dfinfre  10615  dfinfmrOLD  10616  infrenegsup  10618  infmsupOLD  10619  infmrgelbOLD  10622  infmrlbOLD  10624  dfnn2  10649  dflt2  11475  xrinfmss2  11624  infmxrgelbOLD  11653  xrinfm0OLD  11655  fzpr  11879  preduz  11941  predfz  11944  uzrdgfni  12203  axdc4uzlem  12226  axdc4uz  12227  mptnn0fsuppd  12241  seqval  12255  seqfeq4  12293  serle  12299  seqof  12301  hash1snb  12625  hashxplem  12637  hashmap  12639  hashpw  12640  hashfun  12641  hashbclem  12647  hashfacen  12649  hashf1lem1  12650  hashf1lem2  12651  hashf1  12652  fz1isolem  12656  hash2prde  12663  hash2exprb  12664  hash2prb  12665  hashge2el2difr  12670  fi1uzind  12682  brfi1uzind  12683  brfi1indALT  12685  opfi1uzind  12686  wrdexb  12715  ccatfnOLD  12753  wrdind  12869  wrd2ind  12870  cotr2g  13088  trclublem  13107  trclun  13126  rtrclreclem3  13171  dfrtrcl2  13173  relexpindlem  13174  shftfval  13181  shftfib  13183  shftfn  13184  2shfti  13191  sqrlem6  13359  rexfiuz  13458  rlimdm  13663  fclim  13665  climshft  13688  fsumsplitsnun  13864  fsum2dlem  13879  fsumcom2  13883  fsum0diag2  13892  modfsummods  13901  fsumabs  13909  fsumrlim  13919  fsumo1  13920  fsumiun  13929  incexclem  13942  isumltss  13954  supcvg  13962  ntrivcvg  14001  fprodcllemf  14060  fprodfac  14075  fprod2dlem  14082  fprodcom2  14086  bpoly2  14158  bpoly3  14159  rpnnen2lem11  14325  algrf  14580  lcmfunsnlem  14662  lcmfun  14666  isprm2lem  14679  isprm2  14680  prmind2  14683  coprmprod  14726  coprmproddvdslem  14727  iserodd  14833  4sqlem12  14948  vdwlem10  14988  vdwlem13  14991  ramtlecl  14999  hashbc0  15005  ramval  15008  ramvalOLD  15009  ramcl2lemOLD  15011  ramub2  15019  0ram  15026  ram0  15028  ramub1lem1  15032  ramub1lem2  15033  ramub1  15034  restfn  15371  elrest  15374  prdsval  15401  prdsle  15408  prdsless  15409  prdsleval  15423  pwsle  15438  imasaddfnlem  15482  imasvscafn  15491  imasleval  15495  xpsc0  15514  xpsc1  15515  xpsfrnel2  15519  ismre  15544  fnmre  15545  fnmrc  15561  mrcfval  15562  mrisval  15584  mreexexlem4d  15601  isacs2  15607  mreacs  15612  acsfn  15613  acsfn1  15615  acsfn2  15617  cidffn  15632  comfeq  15659  invsym2  15716  oppcsect2  15732  cicsym  15757  brssc  15767  sscpwex  15768  isssc  15773  issubc  15788  isfuncd  15818  cofucl  15841  funcres2b  15850  funcpropd  15853  initoid  15948  termoid  15949  setcmon  16030  catcval  16039  equivestrcsetc  16085  xpcval  16110  xpccatid  16121  curf2ndf  16180  drsdirfi  16231  isdrs2  16232  joinfval  16295  joindmss  16301  meetfval  16309  meetdmss  16315  clatl  16410  odupos  16429  oduposb  16430  oduglb  16433  odulub  16435  posglbd  16444  ipoval  16448  ipolerval  16450  fpwipodrs  16458  ipodrsima  16459  isacs5lem  16463  psdmrn  16501  psssdm2  16509  mrcmndind  16661  pwsdiagmhm  16664  gsumwspan  16678  mulgpropd  16839  eqgfval  16913  eqgval  16914  gicsubgen  16990  gaid  17001  gaorb  17009  orbsta  17015  symgval  17068  symgbas  17069  symgplusg  17078  symg1bas  17085  gsmsymgrfix  17117  symgfixf1  17126  pmtrfval  17139  pmtrrn2  17149  symggen  17159  pmtrprfvalrn  17177  sylow1lem2  17299  sylow2alem1  17317  sylow2alem2  17318  sylow2a  17319  sylow2blem1  17320  sylow2blem2  17321  sylow2blem3  17322  sylow3lem1  17327  sylow3lem6  17332  efgval  17415  efgval2  17422  efgrelexlemb  17448  efgcpbllema  17452  efgcpbllemb  17453  vrgpfval  17464  frgpuplem  17470  qusabl  17551  abln0  17553  frgpnabllem1  17557  gsumval3lem2  17588  gsumzaddlem  17602  gsumzadd  17603  gsum2dlem1  17650  gsum2dlem2  17651  gsum2d  17652  gsum2d2  17654  gsumcom2  17655  gsumxp  17656  telgsums  17671  dprdfadd  17701  dprd2dlem1  17722  dprd2d2  17725  ablfac1eulem  17753  ringn0  17879  opprsubg  17912  subrgpropd  18090  lss1d  18234  pwsdiaglmhm  18328  pwssplit3  18332  lbsextlem4  18432  drngnidl  18501  lidldvgen  18527  psrbaglefi  18644  mplcoe1  18737  mplcoe5lem  18739  mplcoe5  18740  ltbval  18743  ltbwe  18744  opsrle  18747  opsrtoslem1  18755  opsrtoslem2  18756  evlslem4  18779  mpfind  18807  coe1mul2  18910  coe1tm  18914  coe1fzgsumdlem  18943  pf1ind  18991  evl1gsumdlem  18992  znleval  19173  cssmre  19304  thlle  19308  pjfval2  19320  dsmmval  19345  islindf4  19444  lmisfree  19448  gsumcom3  19472  mat1dimelbas  19544  mat1f1o  19551  scmatscm  19586  mat1scmat  19612  mdetdiaglem  19671  mdetunilem7  19691  mdetunilem9  19693  madugsum  19716  chfacfscmulfsupp  19931  chfacfpmmulfsupp  19935  istopon  19988  bastg  20029  tgdom  20042  distop  20059  indistopon  20064  fctop  20067  cctop  20069  ppttop  20070  epttop  20072  fncld  20085  mretopd  20156  toponmre  20157  opnnei  20184  tgrest  20223  resttopon  20225  restco  20228  neitr  20244  ordtbas2  20255  ordtcnv  20265  ordtrest2  20268  pnfnei  20284  mnfnei  20285  iscnp2  20303  subbascn  20318  cnrest2  20350  cnpresti  20352  cnprest  20353  cnprest2  20354  ist1-3  20413  hausnei2  20417  fincmp  20456  cmpsublem  20462  cmpsub  20463  uncmp  20466  fiuncmp  20467  hauscmplem  20469  bwth  20473  dfcon2  20482  consuba  20483  cnconn  20485  uncon  20492  t1conperf  20499  1stcfb  20508  2ndcsb  20512  2ndc1stc  20514  1stcrest  20516  2ndcctbss  20518  2ndcomap  20521  2ndcsep  20522  dis2ndc  20523  subislly  20544  restlly  20546  islly2  20547  hausllycmp  20557  cldllycmp  20558  lly1stc  20559  dislly  20560  hausmapdom  20563  dissnlocfin  20592  comppfsc  20595  kgenf  20604  iskgen3  20612  llycmpkgen2  20613  1stckgenlem  20616  1stckgen  20617  kgencn2  20620  txuni2  20628  txbas  20630  eltx  20631  ptpjpre1  20634  ptpjcn  20674  ptpjopn  20675  ptclsg  20678  dfac14  20681  xkoccn  20682  txcnp  20683  txcnmpt  20687  txrest  20694  txindis  20697  txlly  20699  txnlly  20700  pthaus  20701  txcmplem1  20704  txcmplem2  20705  hausdiag  20708  txlm  20711  tx1stc  20713  tx2ndc  20714  txkgen  20715  xkopt  20718  xkococnlem  20722  xkococn  20723  cnmpt1st  20731  cnmpt2nd  20732  xkofvcn  20747  xkoinjcn  20750  txcon  20752  imasnopn  20753  imasncld  20754  imasncls  20755  basqtop  20774  tgqtop  20775  hmphdis  20859  indishmph  20861  txhmeo  20866  pt1hmeo  20869  ptuncnv  20870  ptunhmeo  20871  xpstopnlem1  20872  ptcmpfi  20876  xkohmeo  20878  isfbas  20892  fbssfi  20900  trfbas2  20906  snfil  20927  fgcl  20941  filcon  20946  fbasrn  20947  trfil2  20950  cfinfil  20956  csdfil  20957  supfil  20958  zfbas  20959  isufil2  20971  acufl  20980  filufint  20983  fin1aufil  20995  rnelfmlem  21015  rnelfm  21016  fmfnfmlem3  21019  fmfnfmlem4  21020  fmfnfm  21021  ufldom  21025  flimrest  21046  hauspwpwf1  21050  txflf  21069  fclsrest  21087  fclscmp  21093  alexsubALTlem2  21111  alexsubALTlem3  21112  alexsubALTlem4  21113  alexsubALT  21114  ptcmplem2  21116  ptcmplem3  21117  ptcmplem4  21118  cnextf  21129  cnextcn  21130  tmdgsum  21158  symgtgp  21164  cldsubg  21173  tgpconcomp  21175  qustgplem  21183  qustgphaus  21185  prdstmdd  21186  tsmsval2  21192  tsmssubm  21205  ustfn  21264  ustfilxp  21275  ustn0  21283  restutopopn  21301  ustuqtop0  21303  ustuqtop1  21304  ustuqtop2  21305  ustuqtop3  21306  ustuqtop4  21307  utopsnneiplem  21310  utopreg  21315  ucnimalem  21343  ucnima  21344  fmucndlem  21354  neipcfilu  21359  imasdsf1olem  21436  xpsdsval  21444  xmetec  21497  prdsbl  21554  stdbdxmet  21578  met1stc  21584  prdsxmslem2  21592  metustid  21617  metustsym  21618  metustexhalf  21619  metustfbas  21620  blval2  21625  metuel2  21628  metustbl  21629  restmetu  21633  xrtgioo  21872  xrsblre  21877  icccmplem1  21888  icccmplem2  21889  fsumcn  21950  fsum2cn  21951  cnllycmp  22032  isphtpc  22073  pi1blem  22118  iscmet3  22311  metcld2  22324  bcthlem4  22343  minveclem3b  22418  minveclem3bOLD  22430  ovolfiniun  22502  ovoliunlem1  22503  ovoliunlem2  22504  finiunmbl  22545  volfiniun  22548  iundisj2  22550  uniioombllem3  22591  vitalilem2  22615  vitalilem3  22616  mbfimaopnlem  22659  itg1addlem4  22705  mbfi1fseqlem4  22724  mbfi1fseqlem6  22726  itgfsum  22832  ellimc2  22880  limcflf  22884  perfdvf  22906  dvres  22914  dvres2  22915  dvnff  22925  dvcj  22952  dvrec  22957  dvmptfsum  22975  dvef  22980  rolle  22990  dvivthlem1  23008  dvfsumle  23021  dvfsumabs  23023  dvfsumlem2  23027  dvfsumlem3  23028  ftc1cn  23043  vieta1lem2  23312  elqaalem2  23321  elqaalem2OLD  23324  ulmdv  23406  logfac  23598  xrlimcnp  23942  jensenlem1  23960  jensenlem2  23961  wilthlem2  24042  prmorcht  24153  lgsquadlem1  24330  lgsquadlem2  24331  dchrisumlem3  24377  istrkg2ld  24556  ishpg  24849  umgraex  25098  isusgra0  25122  usgraop  25125  usgrac  25126  edgss  25127  usgra2edg  25157  usgrarnedg  25159  usgraedg4  25162  usgraedgreu  25163  usgraexmplef  25176  usgrafis  25191  nbgraf1olem5  25221  nb3graprlem1  25227  cusgrarn  25235  cusgrasize  25254  cusgrafilem1  25255  cusgrafilem2  25256  isuvtx  25264  wlkcompim  25302  wlkelwrd  25306  wlkntrllem2  25338  wlkntrl  25340  constr1trl  25366  2pthon  25380  dfconngra1  25447  wlkiswwlk2  25473  wwlkn0s  25481  wlknwwlknsur  25488  wlkiswwlksur  25495  clwlkcompim  25540  erclwwlkref  25589  erclwwlksym  25590  erclwwlktr  25591  erclwwlknref  25601  erclwwlknsym  25602  erclwwlkntr  25603  eclclwwlkn0  25607  eclclwwlkn1  25608  clwlkfoclwwlk  25621  el2wlkonot  25645  el2spthonot  25646  el2spthonot0  25647  usg2wlkonot  25659  usg2wotspth  25660  2wot2wont  25662  2spontn0vne  25663  2spot2iun2spont  25667  0egra0rgra  25712  rusgrasn  25721  rusgranumwlkb0  25729  eupath  25757  frisusgranb  25773  frgra3vlem1  25776  frgra3vlem2  25777  3vfriswmgralem  25780  2pthfrgra  25787  frg2woteq  25836  2spotiundisj  25838  usg2spot2nb  25841  frgraregord013  25894  friendship  25898  ex-natded9.26  25917  nvss  26260  vsfval  26302  h2hlm  26681  axhcompl-zf  26699  hlim2  26893  hhcmpl  26901  hhcms  26904  isch2  26924  helch  26944  hhsscms  26978  occl  27005  chintcli  27032  spanuni  27245  spansni  27258  elnlfn  27629  nmopun  27715  nlelchi  27762  cnlnssadj  27781  adjbd1o  27786  branmfn  27806  pjnmopi  27849  hmopidmchi  27852  foresf1o  28187  rabfodom  28188  abrexss  28194  iuninc  28224  disjabrex  28240  disjabrexf  28241  disjpreima  28242  disjxpin  28246  iundisj2f  28248  fcoinvbr  28263  br8d  28266  iunsnima  28272  suppss2fOLD  28285  suppss2f  28286  fmptdF  28303  fmptcof2  28307  acunirnmpt  28309  acunirnmpt2  28310  acunirnmpt2f  28311  aciunf1lem  28312  ofpreima  28316  funcnvmptOLD  28318  funcnvmpt  28319  dfcnv2  28327  1stpreima  28335  2ndpreima  28336  padct  28355  resf1o  28363  fpwrelmapffslem  28365  xrge0infssOLD  28389  infxrge0glbOLD  28397  iundisj2fi  28421  oduprs  28465  odutos  28472  tosglblem  28478  gsumle  28590  gsummpt2co  28591  gsummpt2d  28592  gsumvsca1  28593  gsumvsca2  28594  psgnfzto1stlem  28661  submateq  28683  lmat22lem  28691  fimaproj  28708  locfinreflem  28715  locfinref  28716  cmpcref  28725  ldlfcntref  28729  pstmxmet  28748  tpr2rico  28766  prsdm  28768  prsrn  28769  ordtcnvNEW  28774  ordtrest2NEW  28777  ordtconlem1  28778  esum0  28918  esumc  28920  esumcst  28932  esumrnmpt2  28937  esumfsup  28939  esumpfinvalf  28945  hasheuni  28954  esum2dlem  28961  esum2d  28962  esumiun  28963  sigaex  28979  isrnsigaOLD  28982  pwsiga  29000  sigainb  29006  insiga  29007  dmsigagen  29014  pwldsys  29027  ldsysgenld  29030  sigapildsyslem  29031  sigapildsys  29032  ldgenpisyslem1  29033  measbase  29067  ismeas  29069  isrnmeas  29070  measiuns  29087  measdivcstOLD  29094  measdivcst  29095  cntmeas  29096  ddemeas  29107  mbfmco2  29135  mbfmcnt  29138  br2base  29139  dya2iocrfn  29149  dya2iocct  29150  dya2iocnrect  29151  dya2iocucvr  29154  sxbrsigalem2  29156  omscl  29167  omsclOLD  29171  oms0  29173  omsmon  29174  omssubadd  29176  oms0OLD  29177  omsmonOLD  29178  omssubaddOLD  29180  fiunelcarsg  29196  carsgclctunlem1  29197  sitgaddlemb  29229  eulerpartlemb  29249  eulerpartlemt  29252  eulerpartgbij  29253  eulerpartlemr  29255  eulerpartlemgvv  29257  eulerpartlemgh  29259  eulerpartlemgs2  29261  eulerpartlemn  29262  sseqf  29273  ballotlemsf1o  29394  ballotlemsf1oOLD  29432  ballotlemircOLD  29450  bnj23  29572  bnj62  29574  bnj219  29589  bnj610  29605  bnj918  29625  bnj927  29628  bnj976  29637  bnj1098  29643  bnj1379  29690  bnj110  29717  bnj98  29726  bnj154  29737  bnj155  29738  bnj535  29749  bnj556  29759  bnj557  29760  bnj591  29770  bnj594  29771  bnj580  29772  bnj607  29775  bnj609  29776  bnj600  29778  bnj849  29784  bnj893  29787  bnj908  29790  bnj934  29794  bnj944  29797  bnj964  29802  bnj966  29803  bnj969  29805  bnj970  29806  bnj910  29807  bnj986  29813  bnj999  29816  bnj1018  29821  bnj907  29824  bnj1039  29828  bnj1040  29829  bnj1052  29832  bnj1123  29843  bnj1030  29844  bnj1133  29846  bnj1128  29847  bnj1145  29850  bnj1204  29869  bnj1373  29887  bnj1417  29898  bnj1421  29899  derangenlem  29942  subfacp1lem1  29950  subfacp1lem3  29953  subfacp1lem4  29954  subfacp1lem5  29955  erdszelem8  29969  erdsze2lem2  29975  kur14lem9  29985  ptpcon  30004  indispcon  30005  conpcon  30006  cnllyscon  30016  cvmsss2  30045  cvmcov2  30046  cvmliftlem15  30069  cvmlift2lem1  30073  cvmlift2lem12  30085  mrsubvrs  30208  msubff1  30242  mclsrcl  30247  mclsppslem  30269  ghomgrplem  30355  untsucf  30385  shftvalg  30413  dftr6  30438  coepr  30440  dffr5  30441  dfso2  30442  dfpo2  30443  br8  30444  br6  30445  br4  30446  dfres3  30447  cnvco1  30448  cnvco2  30449  eldm3  30450  pocnv  30452  socnv  30453  fundmpss  30455  fprb  30461  br1steqg  30464  br2ndeqg  30465  dfdm5  30466  dfrn5  30467  opelco3  30468  elima4  30469  setinds  30472  dfon2lem1  30477  dfon2lem3  30479  dfon2lem6  30482  dfon2lem7  30483  dfon2lem8  30484  dfon2  30486  rdgprc  30489  dfrdg2  30490  trpredrec  30527  poseq  30539  soseq  30540  wzel  30555  wsuclem  30556  frrlem5  30566  frrlem11  30574  sltsolem1  30605  nofulllem5  30643  txpss3v  30693  brtxp  30695  brtxp2  30696  pprodss4v  30699  brpprod  30700  brpprod3a  30701  brpprod3b  30702  brsset  30704  idsset  30705  dfon3  30707  brtxpsd  30709  brbigcup  30713  dfbigcup2  30714  fobigcup  30715  elfix  30718  elfix2  30719  dffix2  30720  fixcnv  30723  dfom5b  30727  sscoid  30728  dffun10  30729  elfuns  30730  elfunsg  30731  elsingles  30733  fnsingle  30734  fvsingle  30735  dfiota3  30738  brimage  30741  brimageg  30742  funimage  30743  fnimage  30744  imageval  30745  brcart  30747  brdomaing  30750  brrangeg  30751  brimg  30752  brapply  30753  brcup  30754  brcap  30755  brsuccf  30756  funpartlem  30757  funpartfun  30758  funpartfv  30760  fullfunfv  30762  brrestrict  30764  dfrecs2  30765  dfrdg4  30766  dfint3  30767  imagesset  30768  brlb  30770  altopelaltxp  30791  altxpsspw  30792  brsegle  30923  fvline  30959  liness  30960  ellines  30967  rankung  30981  ranksng  30982  rankelg  30983  rankpwg  30984  rankeq1o  30986  elhf2g  30991  hfext  30998  trer  31020  finminlem  31022  gtinf  31023  fneer  31057  fnessref  31061  refssfne  31062  neibastop1  31063  tailfb  31081  filnetlem2  31083  filnetlem3  31084  filnetlem4  31085  onsucconi  31145  bj-sbeq  31547  bj-sbel1  31551  bj-snsetex  31601  bj-snglc  31607  bj-0nelsngl  31609  bj-snglex  31611  bj-taginv  31624  bj-df-v  31664  csbdif  31770  f1omptsnlem  31782  topdifinfindis  31793  finxpreclem2  31826  finxp0  31827  finxp1o  31828  finxpreclem5  31831  finxpreclem6  31832  finixpnum  31974  fin2solem  31975  fin2so  31976  ptrest  31983  poimirlem2  31986  poimirlem15  31999  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem24  32008  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  poimirlem28  32012  poimirlem29  32013  poimirlem30  32014  poimirlem31  32015  poimirlem32  32016  heicant  32019  mblfinlem3  32023  mblfinlem4  32024  ismblfin  32025  mbfresfi  32031  ftc1cnnc  32060  ftc1anclem6  32066  areacirclem5  32080  cover2g  32085  f1opr  32095  inixp  32099  indexdom  32105  frinfm  32106  sdclem2  32115  sdclem1  32116  fdc  32118  isbndx  32158  prdstotbnd  32170  heibor1lem  32185  heiborlem1  32187  heiborlem3  32189  heiborlem4  32190  heiborlem5  32191  heiborlem6  32192  heiborlem8  32194  heiborlem10  32196  ismrer1  32214  riscer  32271  divrngidl  32305  intidl  32306  isfldidl  32345  ispridlc  32347  sbccom2  32409  sbccom2f  32410  ac6s6  32459  ac6s6f  32460  prtlem10  32481  prtlem13  32484  prtlem16  32485  prtlem19  32494  prter2  32497  prter3  32498  renegclALT  32579  eqlkr2  32710  glbconxN  32987  pmapglbx  33378  pmapglb  33379  pclclN  33500  pclfinN  33509  polval2N  33515  pclfinclN  33559  osumcllem10N  33574  pexmidlem7N  33585  cdleme31sdnN  33998  cdlemefr44  34036  cdleme48fv  34110  cdleme46fvaw  34112  cdleme48bw  34113  cdleme46fsvlpq  34116  cdlemeg46fvcl  34117  cdlemeg49le  34122  cdlemeg46fjgN  34132  cdlemeg46fjv  34134  cdleme48d  34146  cdlemeg49lebilem  34150  cdleme50eq  34152  cdleme50f  34153  cdlemg2jlemOLDN  34204  cdlemg2klem  34206  cdlemk40  34528  cdlemk56  34582  diaglbN  34667  dvhlveclem  34720  dib1dim  34777  dibglbN  34778  diblss  34782  diblsmopel  34783  dicelvalN  34790  diclspsn  34806  cdlemn7  34815  dihordlem7  34826  dihopelvalcpre  34860  xihopellsmN  34866  dihopellsm  34867  dih1  34898  dihmeetlem1N  34902  dihglblem5apreN  34903  dihmeetlem2N  34911  dihglbcpreN  34912  dihmeetlem4preN  34918  dihmeetlem13N  34931  dih1dimatlem  34941  dihatlat  34946  dihjatcclem4  35033  elrfi  35580  ismrcd2  35585  istopclsd  35586  ismrc  35587  mrefg2  35593  isnacs3  35596  mzpclall  35613  mzpincl  35620  mzpsubst  35634  mzpcompact2lem  35637  mzpcompact2  35638  eldioph2lem1  35646  eldioph2lem2  35647  eldiophss  35661  diophrex  35662  rexrabdioph  35681  2rexfrabdioph  35683  3rexfrabdioph  35684  4rexfrabdioph  35685  6rexfrabdioph  35686  7rexfrabdioph  35687  rabren3dioph  35702  fphpd  35703  rencldnfilem  35707  pellexlem5  35721  pellex  35723  rmxypairf1o  35803  monotuz  35833  monotoddzzfi  35834  oddcomabszz  35836  2nn0ind  35837  zindbi  35838  mzpcong  35866  rmydioph  35913  rmxdioph  35915  expdiophlem2  35921  setindtr  35923  setindtrs  35924  dford3lem2  35926  ttac  35935  pw2f1ocnv  35936  wepwsolem  35944  dnnumch1  35946  fnwe2val  35951  fnwe2lem2  35953  aomclem1  35956  aomclem2  35957  aomclem6  35961  dfac11  35964  kelac2lem  35966  dfac21  35968  islssfg2  35973  lmhmlnmsplit  35989  pwslnmlem1  35994  pwslnm  35996  unxpwdom3  35997  dfacbasgrp  36011  lnr2i  36019  lnrfg  36022  rngunsnply  36083  acsfn1p  36109  idomsubgmo  36116  fgraphxp  36132  areaquad  36145  pwinfi  36212  cllem0  36214  superficl  36215  superuncl  36216  ssficl  36217  ssuncl  36218  ssdifcl  36219  sssymdifcl  36220  elinintrab  36227  inintabss  36228  inintabd  36229  cnvcnvintabd  36250  elcnvlem  36251  cnvintabd  36253  undmrnresiss  36254  cnvssco  36256  intabssd  36260  dfid7  36263  rtrclex  36268  clcnvlem  36274  dfrtrcl5  36280  intima0  36283  elimaint  36284  csbcog  36285  cnviun  36286  imaiun1  36287  coiun1  36288  elintima  36289  trficl  36305  dfrcl2  36310  comptiunov2i  36342  corclrcl  36343  iunrelexpuztr  36355  dftrcl3  36356  cotrcltrcl  36361  brtrclfv2  36363  dfrtrcl3  36369  corcltrcl  36375  cotrclrcl  36378  dfhe3  36414  snhesn  36426  psshepw  36428  frege55lem2c  36557  frege55c  36558  dffrege76  36579  frege81  36584  frege92  36595  frege93  36596  frege95  36598  frege97  36600  frege109  36612  frege110  36613  dffrege115  36618  frege123  36626  frege130  36633  frege131  36634  nzss  36709  expgrowth  36727  2sbc6g  36809  iotain  36811  compel  36834  ipo0  36845  ifr0  36846  onfrALTlem5  36951  onfrALTlem4  36952  onfrALTlem3  36953  opelopab4  36961  ax6e2nd  36968  trsspwALT  37245  trsspwALT2  37246  trsspwALT3  37247  csbingOLD  37254  pwtrVD  37259  unipwrVD  37267  unipwr  37268  onfrALTlem5VD  37321  onfrALTlem4VD  37322  onfrALTlem3VD  37323  relopabVD  37337  ax6e2ndVD  37344  sspwimp  37354  sspwimpVD  37355  sspwimpcf  37356  sspwimpcfVD  37357  sspwimpALT  37361  sspwimpALT2  37364  ax6e2ndALT  37366  fnchoice  37389  fiiuncl  37443  suprnmpt  37476  rnmptpr  37481  wessf1ornlem  37496  disjf1o  37503  disjinfi  37505  ssnnf1octb  37507  projf1o  37511  mapsnd  37513  mapsnend  37517  choicefi  37518  mpct  37519  fzisoeu  37555  upbdrech  37560  infrglbOLD  37706  ellimcabssub0  37734  constlimc  37741  cncfiooicclem1  37808  fprodcncf  37816  dvmptfprod  37857  dvnprodlem1  37858  dvnprodlem2  37859  stoweidlem31  37929  stoweidlem57  37955  stirlinglem13  37985  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem80  38087  fourierdlem93  38100  fourierdlem103  38110  fourierdlem104  38111  etransclem46  38182  pwsal  38213  intsal  38226  salexct  38230  sge00  38255  sge0tsms  38259  sge0fsum  38266  sge0sup  38270  sge0rnbnd  38272  sge0pnffigt  38275  sge0lefi  38277  sge0ltfirp  38279  sge0resplit  38285  sge0split  38288  sge0iunmptlemfi  38292  sge0iunmptlemre  38294  sge0rpcpnf  38300  sge0xp  38308  caratheodorylem2  38385  0ome  38387  hoicvr  38407  hoicvrrex  38415  ovnsubaddlem1  38429  hoidmv1le  38453  hoidmvlelem1  38454  hoidmvlelem2  38455  hoidmvlelem3  38456  hspdifhsp  38475  hspmbllem2  38486  funressnfv  38666  dfdfat2  38670  csbafv12g  38676  tz6.12-afv  38712  rlimdmafv  38716  csbaovg  38719  iccelpart  38784  nnsum3primesgbe  38924  nnsum4primesodd  38928  nnsum4primesoddALTV  38929  iunopeqop  39044  opabn1stprc  39046  funopsn  39059  funop  39060  funop1  39061  funsndifnop  39063  fundmge2nop  39067  fun2dmnopgexmpl  39069  prprrab  39113  hash1n0  39114  fsummmodsndifre  39138  fsummmodsnunz  39139  upgrex  39230  upgr0eopALT  39251  upgr1eopALT  39252  upgrunop  39254  umgrunop  39256  upgredg  39275  umgredg  39276  usgredgreu  39344  uspgredg2vtxeu  39346  ushgredgedga  39355  ushgredgedgaloop  39357  griedg0ssusgr  39386  upgrspanop  39418  umgrspanop  39419  usgrspanop  39420  usgr1v0e  39441  fusgrfis  39445  dfnbgr2  39456  nbuhgr  39460  nbupgr  39461  nbumgrvtx  39463  nbgr2vtx1edg  39467  nbuhgr2vtx1edgb  39469  nb3grprlem1  39503  cplgrop  39553  cusgrsize  39564  cusgrfilem2  39566  fusgrmaxsize  39574  rgrusgrprc  39653  rusgrprc  39654  rgrprcx  39656  umgrislfupgrlem  39717  upgrtrls  39735  upgrspths1wlk  39769  umgr2wlkon  39898  dfconngr1  39928  usgvincvadeu  39989  usgvincvadeuALT  39992  usgedgnlp  39994  usgfis  40030  usgfisALT  40034  c0snmgmhm  40186  rngcvalALTV  40235  ringcvalALTV  40281  opeliun2xp  40386  dmmpt2ssx2  40390  gsumpr  40414  ply1mulgsumlem3  40452  ply1mulgsumlem4  40453  ply1mulgsum  40454  dflinc2  40475  lcosslsp  40503  lmod1zr  40558  lmodn0  40560  lvecpsslmod  40572  nn0sumshdiglem2  40705
  Copyright terms: Public domain W3C validator