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

Theorem oveq2i 6436
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 6433 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-iota 5653  df-fv 5697  df-ov 6428
This theorem is referenced by:  caov32  6634  caov4  6638  caov42  6640  seqomsuc  7314  oa1suc  7373  o2p2e4  7383  om1  7384  oe1  7386  oawordeulem  7396  oeoalem  7438  nnm1  7490  nnm2  7491  nneob  7494  omopthlem1  7497  mapsnconst  7664  mapsncnv  7665  map2xp  7890  cantnflt  8327  cnfcom2  8357  infxpenc  8599  infxpenc2  8603  ackbij1lem5  8804  alephom  9161  pwxpndom2  9241  adderpqlem  9530  addassnq  9534  mulcanenq  9536  distrnq  9537  ltanq  9547  ltexnq  9551  halfnq  9552  ltrnq  9555  archnq  9556  addclprlem2  9593  prlem934  9609  prlem936  9623  addcmpblnr  9644  mulcmpblnrlem  9645  ltsrpr  9652  m1p1sr  9667  m1m1sr  9668  0idsr  9672  1idsr  9673  00sr  9674  pn0sr  9676  recexsrlem  9678  mulgt0sr  9680  sqgt0sr  9681  mulresr  9714  axmulcom  9730  axmulass  9732  axdistr  9733  axi2m1  9734  ax1rid  9736  axcnre  9739  mul02lem1  9962  addid1  9966  negid  10078  negsub  10079  subneg  10080  negsubdii  10116  muleqadd  10419  crne0  10767  2p2e4  10898  3p2e5  10914  3p3e6  10915  4p2e6  10916  4p3e7  10917  4p4e8  10918  5p2e7  10919  5p3e8  10920  5p4e9  10921  5p5e10OLD  10922  6p2e8  10923  6p3e9  10924  6p4e10OLD  10925  7p2e9  10926  7p3e10OLD  10927  8p2e10OLD  10928  3t3e9  10934  8th4div3  11006  halfpm6th  11007  addltmul  11022  div4p1lem1div2  11041  nn0n0n1ge2  11112  nneo  11200  zeo  11202  numsuc  11250  numltc  11267  numsucc  11288  numma  11296  nummul1c  11301  decrmac  11316  decsubi  11322  decsubiOLD  11323  decmul1  11324  decmul10add  11332  decmul10addOLD  11333  6p5lem  11334  5p5e10  11335  6p4e10  11337  7p3e10  11342  8p2e10  11349  4t3lem  11370  9t11e99  11410  9t11e99OLD  11411  decbin2  11422  xmulmnf1  11844  fztp  12134  fzprval  12138  fztpval  12139  fzshftral  12164  fz0tp  12176  fz0to3un2pr  12177  fzo01  12284  fzo12sn  12285  fzo13pr  12286  fzo0to2pr  12287  fzo0to3tp  12288  fzo0to42pr  12289  fzo1to4tp  12290  quoremz  12383  quoremnn0ALT  12385  intfrac2  12386  intfracq  12387  sqval  12651  sqrecii  12675  sq4e2t8  12691  cu2  12692  i3  12695  i4  12696  binom2i  12703  binom3  12714  crreczi  12718  3dec  12779  sq10OLD  12780  3decOLD  12782  nn0opthlem1  12784  facp1  12794  faclbnd  12806  faclbnd2  12807  faclbnd4lem1  12809  faclbnd4lem4  12812  bcn1  12829  bcn2  12835  4bc3eq4  12844  4bc2eq6  12845  hashgadd  12891  hashxplem  12943  hashmap  12945  hashfun  12947  hashbclem  12956  fz1isolem  12965  ccatlid  13079  ccatrid  13080  ccats1val2  13113  ccat2s1p2  13115  wrdeqs1cat  13183  swrdccatin12lem3  13198  swrdccat3a  13202  cats1fvn  13311  cats1cat  13314  cats2cat  13315  s3fn  13363  swrds2  13390  reim0  13563  cji  13604  sqrtm1  13721  absi  13731  rddif  13785  iseraltlem2  14128  iseralt  14130  fsump1i  14209  fsummulc2  14225  incexclem  14274  incexc  14275  arisum2  14299  geoihalfsum  14320  mertenslem1  14322  mertens  14324  risefall0lem  14463  risefac1  14470  fallfac1  14471  fallfacfwd  14473  bpoly0  14487  bpoly1  14488  bpolydiflem  14491  bpoly2  14494  bpoly3  14495  bpoly4  14496  fsumcube  14497  ef0lem  14515  ege2le3  14526  eft0val  14548  ef4p  14549  efgt1p2  14550  efgt1p  14551  tanval2  14569  efival  14588  ef01bndlem  14620  sin01bnd  14621  cos01bnd  14622  cos1bnd  14623  cos2bnd  14624  rpnnen2lem11  14659  sqr2irrlem  14683  3dvdsdec  14759  3dvdsdecOLD  14760  3dvds2dec  14761  3dvds2decOLD  14762  odd2np1lem  14769  odd2np1  14770  oddp1even  14773  opoe  14792  divalglem5OLD  14826  divalglem5  14827  divalglem6  14828  bits0  14858  0bits  14870  gcdaddmlem  14954  6gcd4e2  14964  lcmneg  15028  3lcm2e6woprm  15040  6lcm4e12  15041  3prm  15118  3lcm2e6  15152  phiprm  15196  eulerthlem2  15201  prmdiv  15204  pythagtriplem12  15251  pythagtriplem14  15253  pcmpt  15316  pcfac  15323  prmpwdvds  15328  pockthi  15331  prmreclem2  15341  prmreclem6  15345  4sqlem5  15366  4sqlem13  15381  modxai  15492  mod2xnegi  15495  gcdi  15497  decexp2  15499  numexpp1  15502  numexp2x  15503  decsplit0b  15504  decsplit1  15506  decsplit  15507  decsplit0bOLD  15508  decsplit1OLD  15510  decsplitOLD  15511  2exp16  15517  prmlem0  15532  139prm  15551  163prm  15552  317prm  15553  631prm  15554  1259lem4  15561  1259lem5  15562  1259prm  15563  2503lem1  15564  2503lem2  15565  2503lem3  15566  2503prm  15567  4001lem1  15568  4001lem4  15571  ressinbas  15645  rcaninv  16167  rescfth  16310  xpccatid  16541  oduval  16843  oppgmnd  17497  psgnunilem2  17628  psgnunilem4  17630  psgnpmtr  17643  psgn0fv0  17644  psgnsn  17653  psgnprfval1  17655  lsmmod2  17818  efgi0  17862  efgi1  17863  efginvrel2  17869  efgsval2  17875  efgsp1  17879  efgredleme  17885  efgredlemc  17887  efgcpbllemb  17897  frgpnabllem1  18004  lt6abl  18024  gsumconstf  18063  gsum2dlem2  18098  pwsgsum  18106  fsfnn0gsumfsffz  18107  dprd0  18158  dprdf1  18160  dprd2da  18169  ablfac1lem  18195  pgpfac1lem3  18204  pgpfaclem1  18208  srgbinomlem4  18271  opprring  18359  mulgass3  18365  evlsval  19242  mpff  19256  ply1assa  19292  gsumply1subr  19327  ply1coe  19389  coe1fzgsumdlem  19394  coe1fzgsumd  19395  gsumply1eq  19398  evl1gsumdlem  19443  evl1gsumd  19444  xrsnsgrp  19503  znbas  19615  znzrh2  19617  dsmmval2  19800  frlmip  19837  matgsum  19963  madetsumid  19987  mdetrsca  20129  mdetrsca2  20130  mdettpos  20137  m2detleiblem2  20154  madugsum  20169  madurid  20170  cpmat  20234  pmatcollpwfi  20307  pmatcollpw3fi1lem1  20311  pm2mpval  20320  mp2pm2mplem5  20335  chpmat1dlem  20360  chpmat1d  20361  chpidmat  20372  cpmidpmat  20398  cpmadugsumfi  20402  chcoeffeqlem  20410  cayleyhamilton0  20414  cayleyhamiltonALT  20416  cayleyhamilton1  20417  restin  20681  imacmp  20911  concompcon  20946  uptx  21139  cnpflf2  21515  tmdgsum2  21611  tsmsres  21658  tsmsf1o  21659  tsmsmhm  21660  prdsxmet  21884  resspwsds  21887  prdsxmslem2  22044  metdcn2  22357  metdcn  22358  metdscn2  22374  metdscn2OLD  22389  iimulcn  22466  icchmeo  22469  xrhmeo  22474  cnrehmeo  22481  cnheiborlem  22482  evth  22487  evth2  22488  lebnumlem2  22490  lebnumlem2OLD  22493  reparphti  22529  pcoass  22556  pi1xfrcnv  22589  ipcau2  22709  minveclem4  22875  minveclem4OLD  22887  pjthlem1  22892  ovolunlem1a  22947  unmbl  22988  uniioombl  23039  iblitg  23217  dfitg  23218  itg0  23228  iblcnlem1  23236  itgcnlem  23238  itgabs  23283  limcdif  23322  limccnp  23337  limccnp2  23338  dvexp  23398  dvmptid  23402  dvmptc  23403  dvmptfsum  23418  dveflem  23422  dvsincos  23424  mvth  23435  dvlipcn  23437  dvivthlem1  23451  dvfsumle  23464  dvfsumlem2  23470  itgsubst  23492  tdeglem4  23500  tdeglem2  23501  plypf1  23657  plymullem1  23659  coesub  23702  dgrmulc  23716  fta1lem  23751  vieta1lem1  23754  vieta1lem2  23755  aalioulem4  23782  aaliou3lem3  23791  abelthlem2  23878  abelthlem8  23885  abelthlem9  23886  sinhalfpilem  23907  efhalfpi  23915  cospi  23916  efipi  23917  sin2pi  23919  cos2pi  23920  ef2pi  23921  sin2pim  23929  cos2pim  23930  sinmpi  23931  cosmpi  23932  sinppi  23933  cosppi  23934  sincosq4sgn  23945  tangtx  23949  sincos4thpi  23957  sincos6thpi  23959  sincos3rdpi  23960  pige3  23961  abssinper  23962  efif1olem4  23983  efifo  23985  eff1o  23987  circgrp  23990  circsubm  23991  logneg  24026  logimul  24052  logneg2  24053  dvrelog  24071  logcnlem4  24079  dvlog  24085  dvlog2  24087  logtayl  24094  1cxp  24106  ecxp  24107  cxpsqrt  24137  dvsqrt  24171  dvcnsqrt  24173  root1eq1  24184  cxpeq  24186  elogb  24196  ang180lem1  24227  ang180lem2  24228  heron  24253  1cubrlem  24256  1cubr  24257  dcubic2  24259  mcubic  24262  cubic2  24263  binom4  24265  dquartlem1  24266  dquartlem2  24267  dquart  24268  quart1lem  24270  quart1  24271  quartlem1  24272  asinsin  24307  asin1  24309  acos1  24310  atanlogsublem  24330  atanlogsub  24331  efiatan2  24332  2efiatan  24333  tanatan  24334  atanbnd  24341  atan1  24343  dvatan  24350  atantayl2  24353  leibpilem2  24356  leibpi  24357  log2cnv  24359  log2tlbnd  24360  log2ublem1  24361  log2ublem2  24362  log2ublem3  24363  log2ub  24364  birthday  24369  amgmlem  24404  emcllem5  24414  lgamgulmlem2  24444  lgamgulmlem5  24447  lgam1  24478  wilthlem2  24483  ftalem6  24494  basellem2  24498  basellem3  24499  basellem5  24501  basellem8  24504  cht1  24581  chp1  24583  1sgmprm  24614  ppiublem2  24618  ppiub  24619  chtublem  24626  chtub  24627  logfacbnd3  24638  bcp1ctr  24694  bclbnd  24695  bposlem1  24699  bposlem4  24702  bposlem6  24704  bposlem8  24706  bposlem9  24707  lgslem1  24712  lgsdir2lem1  24740  lgsdir2lem2  24741  lgsdir2lem3  24742  lgsdir2lem5  24744  lgs1  24756  gausslemma2dlem1a  24780  gausslemma2dlem3  24783  gausslemma2dlem4  24784  gausslemma2d  24789  lgseisenlem1  24790  lgseisenlem3  24792  lgsquadlem1  24795  lgsquadlem2  24796  lgsquad2lem2  24800  m1lgs  24803  2lgslem1a2  24805  2sqlem8  24841  2sqblem  24846  logdivsum  24912  mulog2sumlem2  24914  log2sumbnd  24923  selberglem1  24924  selberglem2  24925  pntrmax  24943  pntibndlem2  24970  pntibndlem3  24971  pntlemg  24977  pntlemr  24981  pntlemo  24986  ostth2lem3  25014  ostth2lem4  25015  istrkg3ld  25050  trgcgrg  25101  tgcgr4  25117  colperpexlem1  25313  ax5seglem7  25506  axlowdimlem4  25516  axlowdimlem16  25528  0wlk  25814  0trl  25815  wlkntrllem2  25829  wlkntrl  25831  constr1trl  25857  1pthonlem1  25858  constr2wlk  25867  constr2trl  25868  wlkdvspthlem  25876  constr3trllem3  25919  constr3trllem4  25920  constr3trllem5  25921  constr3pthlem1  25922  constr3pthlem3  25924  clwwlkn2  26042  clwlkisclwwlk2  26057  wwlkext2clwwlk  26070  vdgr1c  26171  nbhashuvtx1  26181  vdegp1ai  26250  vdegp1bi  26251  vdegp1ci  26252  extwwlkfablem2  26344  numclwwlkovf2ex  26352  numclwlk2lem2f  26369  frgraregord013  26384  ex-exp  26438  ex-bc  26440  ex-gcd  26445  ex-lcm  26446  ex-ind-dvds  26449  smcnlem  26710  ipidsq  26726  dipcj  26730  dip0r  26733  nmlnoubi  26814  nmblolbii  26817  blocnilem  26822  ip1ilem  26844  ip2i  26846  ipdirilem  26847  ipasslem10  26857  ipasslem11  26858  siilem1  26869  hvmul0  27054  hvsubsub4i  27089  hvnegdii  27092  hvsubeq0i  27093  hvsubcan2i  27094  hvsubaddi  27096  hvsub0  27106  hisubcomi  27134  normlem0  27139  normlem1  27140  normlem2  27141  normlem3  27142  normlem9  27148  norm-ii-i  27167  norm3difi  27177  normpari  27184  polid2i  27187  polidi  27188  bcsiALT  27209  pjhthlem1  27423  chdmm3i  27511  chdmm4i  27512  chjidm  27552  chj4i  27555  chjjdiri  27556  spanunsni  27611  pjoml4i  27619  cmcm2i  27625  qlax4i  27662  qlax5i  27663  pjadjii  27706  pjmulii  27709  pjsubii  27710  pjssmii  27713  pjcji  27716  pjneli  27755  hoadd32i  27810  ho0subi  27827  hosubid1  27830  hosd2i  27855  hopncani  27856  hosubeq0i  27858  lnopeq0lem1  28037  lnopunilem1  28042  lnophmlem2  28049  nmbdoplbi  28056  nmcopexi  28059  lnfnmuli  28076  nmcfnexi  28083  nmoptri2i  28131  nmopcoadji  28133  golem1  28303  mdsl1i  28353  cvmdi  28356  mdslmd3i  28364  csmdsymi  28366  xrge00  28814  archirngz  28871  archiabllem2c  28877  gsumle  28907  gsummpt2co  28908  gsumvsca1  28910  gsumvsca2  28911  xrge0slmod  28972  psgnfzto1st  28983  lmat22det  29013  madjusmdetlem4  29021  raddcn  29100  xrge0iifhom  29108  xrge0mulc1cn  29112  cbvesum  29228  gsumesum  29245  esumpfinvallem  29260  esumpfinvalf  29262  dya2icoseg  29463  sitg0  29543  eulerpartlemd  29563  eulerpartlemgvv  29573  eulerpartlemgh  29575  fib0  29596  fib1  29597  fibp1  29598  orrvcval4  29661  orrvcoel  29662  orrvccel  29663  coinflipprob  29676  coinflippvt  29681  ballotlem2  29685  ballotth  29734  ballotthOLD  29772  signstf0  29817  signstfvn  29818  signsvtn0  29819  signstfvp  29820  signstfveq0  29826  signsvf0  29829  signsvf1  29830  signsvfn  29831  signshf  29837  subfacp1lem1  30261  subfacp1lem5  30266  subfacval2  30269  subfaclim  30270  subfacval3  30271  cvxpcon  30324  cvxscon  30325  mrsub0  30513  problem4  30660  quad3  30662  sinccvglem  30664  iexpire  30717  faclimlem1  30725  frrlem5  30864  fwddifnp1  31278  knoppcnlem10  31497  knoppndvlem7  31514  knoppndvlem21  31528  cnndvlem1  31533  finxpreclem4  32239  ptrest  32453  poimirlem27  32481  dvtan  32505  itgabsnc  32524  ftc1anclem8  32537  dvasin  32541  dvacos  32542  areacirclem1  32545  areacirclem4  32548  areacirc  32550  prdstotbnd  32638  prdsbnd2  32639  repwsmet  32678  rrnequiv  32679  reheibor  32683  dalem-cly  33850  pmodN  34029  cdleme0cp  34394  cdleme0cq  34395  cdleme1  34407  cdleme3d  34411  cdleme3h  34415  cdleme4  34418  cdleme5  34420  cdleme7a  34423  cdleme8  34430  cdleme9  34433  cdleme10  34434  cdleme11g  34445  cdleme15b  34455  cdleme21  34518  cdleme22e  34525  cdleme22eALTN  34526  cdleme23c  34532  cdleme25cv  34539  cdleme35b  34631  cdleme35c  34632  cdleme42a  34652  cdleme42d  34654  cdleme43aN  34670  cdlemeg46gfv  34711  cdlemk35  35093  dihjatcclem1  35600  lcdval2  35772  mapdpglem21  35874  mapfzcons  36172  mapfzcons1cl  36174  2rexfrabdioph  36253  3rexfrabdioph  36254  4rexfrabdioph  36255  6rexfrabdioph  36256  7rexfrabdioph  36257  rabdiophlem2  36259  diophren  36270  rabren3dioph  36272  pellexlem5  36290  pell1qr1  36328  rmspecfund  36367  jm2.17a  36420  jm2.17b  36421  jm2.27c  36467  jm2.27dlem5  36473  lmhmlnmsplit  36550  arearect  36702  areaquad  36703  relexp2  36870  trclfvdecomr  36921  k0004val0  37354  inductionexd  37355  unitadd  37402  amgm2d  37405  amgm3d  37406  lhe4.4ex1a  37432  expgrowthi  37436  expgrowth  37438  bccn1  37447  binomcxplemdvbinom  37456  binomcxplemdvsum  37458  binomcxplemnotnn0  37459  binomcxp  37460  refsumcn  38094  unirnmapsn  38285  oddfl  38315  infleinflem2  38414  sumnnodd  38583  cosnegpi  38637  dvcosre  38686  dvsinax  38688  ioodvbdlimc1lem2  38709  ioodvbdlimc1lem2OLD  38711  ioodvbdlimc2lem  38713  ioodvbdlimc2lemOLD  38714  dvmptmulf  38717  dvxpaek  38720  dvmptfprod  38725  dvnprodlem2  38727  dvnprodlem3  38728  itgsin0pilem1  38731  itgsinexplem1  38735  itgsubsticclem  38757  stoweidlem13  38796  wallispilem4  38851  wallispi2lem1  38854  wallispi2lem2  38855  stirlinglem1  38857  dirkerper  38879  dirkertrigeqlem1  38881  dirkertrigeqlem3  38883  dirkertrigeq  38884  dirkeritg  38885  dirkercncflem1  38886  dirkercncflem2  38887  fourierdlem36  38927  fourierdlem41  38932  fourierdlem42  38933  fourierdlem42OLD  38934  fourierdlem48  38939  fourierdlem56  38947  fourierdlem57  38948  fourierdlem58  38949  fourierdlem60  38951  fourierdlem61  38952  fourierdlem62  38953  fourierdlem65  38956  fourierdlem73  38964  fourierdlem80  38971  fourierdlem87  38978  fourierdlem89  38980  fourierdlem90  38981  fourierdlem91  38982  fourierdlem100  38991  fourierdlem103  38994  fourierdlem107  38998  fourierdlem112  39003  fourierdlem113  39004  fourierdlem115  39006  fouriercnp  39011  sqwvfoura  39013  sqwvfourb  39014  fourierswlem  39015  fouriersw  39016  etransclem2  39022  etransclem37  39057  etransclem46  39066  hoidmvlelem3  39381  vonioolem2  39466  issmflem  39507  smfmullem2  39571  1t10e1p1e11  39832  1t10e1p1e11OLD  39833  fmtno0  39885  fmtno1  39886  fmtnorec2lem  39887  fmtnorec3  39893  fmtno2  39895  fmtno3  39896  fmtno4  39897  fmtno4sqrt  39916  fmtno4prmfac  39917  2exp5  39940  139prmALT  39944  31prm  39945  2exp7  39947  2exp11  39950  mod42tp1mod8  39952  lighneallem2  39956  5tcu2e40  39965  3exp4mod41  39966  41prothprmlem1  39967  41prothprmlem2  39968  41prothprm  39969  bits0ALTV  40023  nnsum3primes4  40099  nnsum3primesgbe  40103  nnsum4primesodd  40107  nnsum4primesoddALTV  40108  nnsum4primeseven  40111  nnsum4primesevenALTV  40112  bgoldbtbndlem1  40116  tgoldbachlt  40125  tgoldbachltOLD  40132  pfx1  40169  pfxccatpfx1  40185  pfxccatpfx2  40186  uhgrstrrepe  40396  vdegp1ci-av  40846  1wlkp1lem6  40979  1wlkp1lem8  40981  1wlkp1  40982  uhgr1wlkspthlem2  41052  pthdlem1  41064  pthdlem2  41066  pthd  41067  crctcsh1wlkn0lem4  41108  crctcsh1wlkn0lem5  41109  crctcsh1wlkn0lem6  41110  crctcshlem4  41115  crctcsh1wlkn0  41116  21wlkdlem2  41225  21wlkdlem4  41227  2pthdlem1  41229  clwlkclwwlk2  41304  wwlksext2clwwlk  41323  0ewlk  41374  1ewlk  41375  01wlk  41376  1pthdlem1  41394  1pthdlem2  41395  11wlkdlem1  41396  11wlkdlem4  41399  1wlk2v2e  41416  31wlkdlem2  41419  31wlkdlem4  41421  3pthdlem1  41423  eupth0  41474  eupthp1  41476  eucrctshift  41503  eucrct2eupth  41505  av-extwwlkfablem1  41600  av-extwwlkfablem2  41602  av-numclwwlkovf2ex  41609  av-numclwlk2lem2f  41625  av-frgraregord013  41641  2t6m3t4e0  42011  zlmodzxzequa  42171  zlmodzxznm  42172  zlmodzxzequap  42174  nn0sumshdiglemA  42303  nn0sumshdiglemB  42304  nn0sumshdiglem1  42305  sec0  42353  dfdp2OLD  42360  amgmw2d  42412
  Copyright terms: Public domain W3C validator