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

Theorem oveq2i 7159
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 7156 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151
This theorem is referenced by:  caov32  7367  caov4  7371  caov42  7373  seqomsuc  8085  oa1suc  8148  o2p2e4  8158  o2p2e4OLD  8159  om1  8160  oe1  8162  oawordeulem  8172  oeoalem  8214  nnm1  8267  nnm2  8268  nneob  8271  omopthlem1  8274  mapsnconst  8448  mapsncnv  8449  map2xp  8679  cantnflt  9127  cnfcom2  9157  infxpenc  9436  infxpenc2  9440  mapdjuen  9598  ackbij1lem5  9638  alephom  9999  pwxpndom2  10079  adderpqlem  10368  addassnq  10372  mulcanenq  10374  distrnq  10375  ltanq  10385  ltexnq  10389  halfnq  10390  ltrnq  10393  archnq  10394  addclprlem2  10431  prlem934  10447  prlem936  10461  addcmpblnr  10483  mulcmpblnrlem  10484  ltsrpr  10491  m1p1sr  10506  m1m1sr  10507  0idsr  10511  1idsr  10512  00sr  10513  pn0sr  10515  recexsrlem  10517  mulgt0sr  10519  sqgt0sr  10520  mulresr  10553  axmulcom  10569  axmulass  10571  axdistr  10572  axi2m1  10573  ax1rid  10575  axcnre  10578  mul02lem1  10808  addid1  10812  negid  10925  negsub  10926  subneg  10927  negsubdii  10963  muleqadd  11276  crne0  11623  2p2e4  11764  1p2e3  11772  3p2e5  11780  3p3e6  11781  4p2e6  11782  4p3e7  11783  4p4e8  11784  5p2e7  11785  5p3e8  11786  5p4e9  11787  6p2e8  11788  6p3e9  11789  7p2e9  11790  3t3e9  11796  8th4div3  11849  halfpm6th  11850  addltmul  11865  div4p1lem1div2  11884  nn0n0n1ge2  11954  nneo  12058  zeo  12060  numsuc  12104  numltc  12116  numsucc  12130  numma  12134  nummul1c  12139  decrmac  12148  decsubi  12153  decmul10add  12159  6p5lem  12160  5p5e10  12161  6p4e10  12162  7p3e10  12165  8p2e10  12170  4t3lem  12187  9t11e99  12220  decbin2  12231  xmulmnf1  12661  fztp  12955  fz12pr  12956  fztpval  12961  fzshftral  12987  fz0tp  13000  fz0to3un2pr  13001  fzo01  13111  fzo12sn  13112  fzo13pr  13113  fzo0to2pr  13114  fzo0to3tp  13115  fzo0to42pr  13116  fzo1to4tp  13117  fzosplitprm1  13139  quoremz  13215  quoremnn0ALT  13217  intfrac2  13218  intfracq  13219  sqval  13473  sqrecii  13538  sq4e2t8  13554  cu2  13555  i3  13558  i4  13559  binom2i  13566  binom3  13577  crreczi  13581  3dec  13618  nn0opthlem1  13620  facp1  13630  faclbnd  13642  faclbnd2  13643  faclbnd4lem1  13645  faclbnd4lem4  13648  bcn1  13665  bcn2  13671  4bc3eq4  13680  4bc2eq6  13681  hashgadd  13730  hashxplem  13786  hashmap  13788  hashfun  13790  hashbclem  13802  fz1isolem  13811  ccatlid  13932  ccatrid  13933  ccatws1len  13966  ccats1val2  13975  ccat2s1p2  13978  ccat2s1p2OLD  13980  pfx1  14057  pfxccatin12lem3  14086  pfxccatpfx1  14090  pfxccatpfx2  14091  cats1fvn  14212  cats1cat  14215  cats2cat  14216  s3fn  14265  swrds2  14294  swrds2m  14295  reim0  14469  cji  14510  sqrtm1  14627  absi  14638  rddif  14692  iseraltlem2  15031  iseralt  15033  fsump1i  15116  fsummulc2  15131  incexclem  15183  incexc  15184  arisum2  15208  geoihalfsum  15230  mertenslem1  15232  mertens  15234  risefall0lem  15372  risefac1  15379  fallfac1  15380  fallfacfwd  15382  bpoly0  15396  bpoly1  15397  bpolydiflem  15400  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  ef0lem  15424  ege2le3  15435  eft0val  15457  ef4p  15458  efgt1p2  15459  efgt1p  15460  tanval2  15478  efival  15497  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos1bnd  15532  cos2bnd  15533  rpnnen2lem11  15569  3dvdsdec  15673  3dvds2dec  15674  odd2np1lem  15681  odd2np1  15682  oddp1even  15685  opoe  15704  divalglem5  15740  divalglem6  15741  bits0  15769  0bits  15780  gcdaddmlem  15864  6gcd4e2  15878  lcmneg  15939  3lcm2e6woprm  15951  6lcm4e12  15952  3prm  16030  3lcm2e6  16064  phiprm  16106  eulerthlem2  16111  prmdiv  16114  pythagtriplem12  16155  pythagtriplem14  16157  pcmpt  16220  pcfac  16227  prmpwdvds  16232  pockthi  16235  prmreclem2  16245  prmreclem6  16249  4sqlem5  16270  4sqlem13  16285  modxai  16396  mod2xnegi  16399  gcdi  16401  decexp2  16403  numexpp1  16406  numexp2x  16407  decsplit0b  16408  decsplit1  16410  decsplit  16411  2exp16  16416  prmlem0  16431  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem4  16469  ressinbas  16552  rcaninv  17056  rescfth  17199  xpccatid  17430  oduval  17732  oppgmnd  18474  psgnunilem2  18615  psgnunilem4  18617  psgnpmtr  18630  psgn0fv0  18631  psgnsn  18640  psgnprfval1  18642  lsmmod2  18794  efgi0  18838  efgi1  18839  efginvrel2  18845  efgsval2  18851  efgsp1  18855  efgredleme  18861  efgredlemc  18863  efgcpbllemb  18873  frgpnabllem1  18985  lt6abl  19007  gsumconstf  19047  gsum2dlem2  19083  pwsgsum  19094  fsfnn0gsumfsffz  19095  dprd0  19145  dprdf1  19147  dprd2da  19156  ablfac1lem  19182  pgpfac1lem3  19191  pgpfaclem1  19195  srgbinomlem4  19285  opprring  19373  mulgass3  19379  evlsval  20291  mpff  20309  ply1assa  20359  gsumply1subr  20394  ply1coe  20456  coe1fzgsumdlem  20461  coe1fzgsumd  20462  gsumply1eq  20465  evl1gsumdlem  20511  evl1gsumd  20512  xrsnsgrp  20573  znbas  20682  znzrh2  20684  dsmmval2  20872  frlmip  20914  matgsum  21038  madetsumid  21062  mdetrsca  21204  mdetrsca2  21205  mdettpos  21212  m2detleiblem2  21229  madugsum  21244  madurid  21245  cpmat  21309  pmatcollpwfi  21382  pmatcollpw3fi1lem1  21386  pm2mpval  21395  mp2pm2mplem5  21410  chpmat1dlem  21435  chpmat1d  21436  chpidmat  21447  cpmidpmat  21473  cpmadugsumfi  21477  chcoeffeqlem  21485  cayleyhamilton0  21489  cayleyhamiltonALT  21491  cayleyhamilton1  21492  restin  21766  imacmp  21997  conncompconn  22032  uptx  22225  cnpflf2  22600  tmdgsum2  22696  tsmsres  22744  tsmsf1o  22745  tsmsmhm  22746  prdsxmet  22971  resspwsds  22974  prdsxmslem2  23131  tngngpim  23260  metdcn2  23439  metdcn  23440  metdscn2  23457  iimulcn  23534  icchmeo  23537  xrhmeo  23542  cnrehmeo  23549  cnheiborlem  23550  evth  23555  evth2  23556  lebnumlem2  23558  reparphti  23593  pcoass  23620  pi1xfrcnv  23653  ipcau2  23829  ehl0base  24011  minveclem4  24027  pjthlem1  24032  ovolunlem1a  24089  unmbl  24130  uniioombl  24182  iblitg  24361  dfitg  24362  itg0  24372  iblcnlem1  24380  itgcnlem  24382  itgabs  24427  limcdif  24466  limccnp  24481  limccnp2  24482  dvexp  24542  dvmptid  24546  dvmptc  24547  dvmptfsum  24564  dveflem  24568  dvsincos  24570  mvth  24581  dvlipcn  24583  dvivthlem1  24597  dvfsumle  24610  dvfsumlem2  24616  itgsubst  24638  tdeglem4  24646  tdeglem2  24647  plypf1  24794  plymullem1  24796  coesub  24839  dgrmulc  24853  fta1lem  24888  vieta1lem1  24891  vieta1lem2  24892  aalioulem4  24916  aaliou3lem3  24925  abelthlem2  25012  abelthlem8  25019  abelthlem9  25020  sinhalfpilem  25041  efhalfpi  25049  cospi  25050  efipi  25051  sin2pi  25053  cos2pi  25054  ef2pi  25055  sin2pim  25063  cos2pim  25064  sinmpi  25065  cosmpi  25066  sinppi  25067  cosppi  25068  sincosq4sgn  25079  tangtx  25083  sincos4thpi  25091  sincos6thpi  25093  sincos3rdpi  25094  pige3ALT  25097  abssinper  25098  efif1olem4  25121  efifo  25123  eff1o  25125  circgrp  25128  circsubm  25129  logneg  25163  logimul  25189  logneg2  25190  dvrelog  25212  logcnlem4  25220  dvlog  25226  dvlog2  25228  logtayl  25235  1cxp  25247  ecxp  25248  cxpsqrt  25278  2irrexpq  25305  dvsqrt  25315  dvcnsqrt  25317  root1eq1  25328  cxpeq  25330  elogb  25340  2logb9irrALT  25368  ang180lem1  25379  ang180lem2  25380  heron  25408  1cubrlem  25411  1cubr  25412  dcubic2  25414  mcubic  25417  cubic2  25418  binom4  25420  dquartlem1  25421  dquartlem2  25422  dquart  25423  quart1lem  25425  quart1  25426  quartlem1  25427  asinsin  25462  asin1  25464  acos1  25465  atanlogsublem  25485  atanlogsub  25486  efiatan2  25487  2efiatan  25488  tanatan  25489  atanbnd  25496  atan1  25498  dvatan  25505  atantayl2  25508  leibpilem2  25511  leibpi  25512  log2cnv  25514  log2tlbnd  25515  log2ublem1  25516  log2ublem2  25517  log2ublem3  25518  log2ub  25519  birthday  25524  amgmlem  25559  emcllem5  25569  lgamgulmlem2  25599  lgamgulmlem5  25602  lgam1  25633  wilthlem2  25638  ftalem6  25647  basellem2  25651  basellem3  25652  basellem5  25654  basellem8  25657  cht1  25734  chp1  25736  1sgmprm  25767  ppiublem2  25771  ppiub  25772  chtublem  25779  chtub  25780  logfacbnd3  25791  bcp1ctr  25847  bclbnd  25848  bposlem4  25855  bposlem6  25857  bposlem8  25859  bposlem9  25860  lgslem1  25865  lgsdir2lem1  25893  lgsdir2lem2  25894  lgsdir2lem3  25895  lgsdir2lem5  25897  lgs1  25909  gausslemma2dlem1a  25933  gausslemma2dlem3  25936  gausslemma2dlem4  25937  gausslemma2d  25942  lgseisenlem1  25943  lgseisenlem3  25945  lgsquadlem1  25948  lgsquadlem2  25949  lgsquad2lem2  25953  m1lgs  25956  2lgslem1a2  25958  2sqlem8  25994  2sqblem  25999  addsq2nreurex  26012  logdivsum  26101  mulog2sumlem2  26103  log2sumbnd  26112  selberglem1  26113  selberglem2  26114  pntrmax  26132  pntibndlem2  26159  pntibndlem3  26160  pntlemg  26166  pntlemr  26170  pntlemo  26175  ostth2lem3  26203  ostth2lem4  26204  istrkg3ld  26239  trgcgrg  26293  tgcgr4  26309  colperpexlem1  26508  ax5seglem7  26713  axlowdimlem16  26735  setsiedg  26813  vdegp1ci  27312  finsumvtxdg2sstep  27323  finsumvtxdg2size  27324  wlkp1lem6  27452  wlkp1lem8  27454  wlkp1  27455  uhgrwkspthlem2  27527  pthdlem1  27539  pthdlem2  27541  pthd  27542  crctcshwlkn0lem4  27583  crctcshwlkn0lem5  27584  crctcshwlkn0lem6  27585  crctcshlem4  27590  crctcshwlkn0  27591  2wlkdlem2  27697  2wlkdlem4  27699  2pthdlem1  27701  wwlks2onv  27724  clwlkclwwlk2  27773  clwwlkwwlksb  27825  wwlksext2clwwlk  27828  clwwlknonex2lem1  27878  0ewlk  27885  1ewlk  27886  0wlk  27887  1pthdlem1  27906  1pthdlem2  27907  1wlkdlem1  27908  1wlkdlem4  27911  wlk2v2e  27928  3wlkdlem2  27931  3wlkdlem4  27933  3pthdlem1  27935  eupth0  27985  eupthp1  27987  eucrctshift  28014  eucrct2eupth  28016  numclwwlk1lem2foalem  28122  numclwlk2lem2f  28148  frgrregord013  28166  ex-exp  28221  ex-bc  28223  ex-gcd  28228  ex-lcm  28229  ex-ind-dvds  28232  smcnlem  28466  ipidsq  28479  dipcj  28483  dip0r  28486  nmlnoubi  28565  nmblolbii  28568  blocnilem  28573  ip1ilem  28595  ip2i  28597  ipdirilem  28598  ipasslem10  28608  ipasslem11  28609  siilem1  28620  hvmul0  28793  hvsubsub4i  28828  hvnegdii  28831  hvsubeq0i  28832  hvsubcan2i  28833  hvsubaddi  28835  hvsub0  28845  hisubcomi  28873  normlem0  28878  normlem1  28879  normlem2  28880  normlem3  28881  normlem9  28887  norm-ii-i  28906  norm3difi  28916  normpari  28923  polid2i  28926  polidi  28927  bcsiALT  28948  pjhthlem1  29160  chdmm3i  29248  chdmm4i  29249  chjidm  29289  chj4i  29292  chjjdiri  29293  spanunsni  29348  pjoml4i  29356  cmcm2i  29362  qlax4i  29399  qlax5i  29400  pjadjii  29443  pjmulii  29446  pjsubii  29447  pjssmii  29450  pjcji  29453  pjneli  29492  hoadd32i  29547  ho0subi  29564  hosubid1  29567  hosd2i  29592  hopncani  29593  hosubeq0i  29595  lnopeq0lem1  29774  lnopunilem1  29779  lnophmlem2  29786  nmbdoplbi  29793  nmcopexi  29796  lnfnmuli  29813  nmcfnexi  29820  nmoptri2i  29868  nmopcoadji  29870  golem1  30040  mdsl1i  30090  cvmdi  30093  mdslmd3i  30101  csmdsymi  30103  dfdec100  30539  dp20u  30547  dpmul10  30564  dpmul100  30566  dp3mul10  30567  dpmul1000  30568  dpexpp1  30577  0dp2dp  30578  dpmul  30582  dpmul4  30583  1mhdrd  30585  s2rn  30613  s3rn  30615  s3f1  30616  cshw1s2  30627  xrge00  30666  gsummpt2co  30679  gsumle  30718  psgnfzto1st  30740  cyc2fv1  30756  cycpmco2lem5  30765  cycpmco2lem6  30766  cycpmco2  30768  cyc3fv1  30772  cyc3fv2  30773  archirngz  30811  archiabllem2c  30817  gsumvsca1  30847  gsumvsca2  30848  xrge0slmod  30910  fply1  30924  lbsdiflsp0  31010  fedgmul  31015  ccfldextrr  31026  lmat22det  31075  madjusmdetlem4  31083  raddcn  31160  xrge0iifhom  31168  xrge0mulc1cn  31172  cbvesum  31289  gsumesum  31306  esumpfinvallem  31321  esumpfinvalf  31323  dya2icoseg  31523  sitg0  31592  eulerpartlemd  31612  eulerpartlemgvv  31622  eulerpartlemgh  31624  fib0  31645  fib1  31646  fibp1  31647  orrvcval4  31710  orrvcoel  31711  orrvccel  31712  coinflipprob  31725  coinflippvt  31730  ballotlem2  31734  ballotth  31783  signstf0  31826  signstfvn  31827  signsvtn0  31828  signstfvp  31829  signstfveq0  31835  signsvf0  31838  signsvf1  31839  signsvfn  31840  prodfzo03  31862  itgexpif  31865  repr0  31870  hgt750lemd  31907  hgt750lem  31910  hgt750lem2  31911  subfacp1lem1  32414  subfacp1lem5  32419  subfacval2  32422  subfaclim  32423  subfacval3  32424  cvxpconn  32477  cvxsconn  32478  sate0  32650  mrsub0  32751  problem4  32899  quad3  32901  sinccvglem  32903  iexpire  32955  faclimlem1  32963  fprlem1  33125  frrlem15  33130  fwddifnp1  33614  knoppcnlem10  33829  knoppndvlem7  33845  knoppndvlem21  33859  cnndvlem1  33864  finxpreclem4  34662  ptrest  34878  poimirlem27  34906  dvtan  34929  itgabsnc  34948  ftc1anclem8  34961  dvasin  34965  dvacos  34966  areacirclem1  34969  areacirclem4  34972  areacirc  34974  prdstotbnd  35059  prdsbnd2  35060  repwsmet  35099  rrnequiv  35100  reheibor  35104  dalem-cly  36794  pmodN  36973  cdleme0cp  37337  cdleme0cq  37338  cdleme1  37350  cdleme3d  37354  cdleme3h  37358  cdleme4  37361  cdleme5  37363  cdleme7a  37366  cdleme8  37373  cdleme9  37376  cdleme10  37377  cdleme11g  37388  cdleme15b  37398  cdleme21  37460  cdleme22e  37467  cdleme22eALTN  37468  cdleme23c  37474  cdleme25cv  37481  cdleme35b  37573  cdleme35c  37574  cdleme42a  37594  cdleme42d  37596  cdleme43aN  37612  cdlemeg46gfv  37653  cdlemk35  38035  dihjatcclem1  38541  lcdval2  38713  mapdpglem21  38815  sqsumi  39152  sqmid3api  39154  sqn5ii  39157  sq3deccom12  39161  re1m1e0m0  39212  sn-00idlem1  39213  remul02  39220  resubid  39223  mapfzcons  39298  mapfzcons1cl  39300  2rexfrabdioph  39378  3rexfrabdioph  39379  4rexfrabdioph  39380  6rexfrabdioph  39381  7rexfrabdioph  39382  rabdiophlem2  39384  diophren  39395  rabren3dioph  39397  pellexlem5  39415  pell1qr1  39453  rmspecfund  39491  jm2.17a  39542  jm2.17b  39543  jm2.27c  39589  jm2.27dlem5  39595  lmhmlnmsplit  39672  arearect  39807  areaquad  39808  relexp2  40007  trclfvdecomr  40058  k0004val0  40489  inductionexd  40490  unitadd  40533  amgm2d  40536  amgm3d  40537  lhe4.4ex1a  40646  expgrowthi  40650  expgrowth  40652  bccn1  40661  binomcxplemdvbinom  40670  binomcxplemdvsum  40672  binomcxplemnotnn0  40673  binomcxp  40674  refsumcn  41272  unirnmapsn  41461  oddfl  41527  infleinflem2  41623  sumnnodd  41895  cosnegpi  42132  dvcosre  42180  dvsinax  42181  ioodvbdlimc1lem2  42201  ioodvbdlimc2lem  42203  dvmptmulf  42206  dvxpaek  42209  dvmptfprod  42214  dvnprodlem2  42216  dvnprodlem3  42217  itgsin0pilem1  42219  itgsinexplem1  42223  itgsubsticclem  42244  stoweidlem13  42283  wallispilem4  42338  wallispi2lem1  42341  wallispi2lem2  42342  stirlinglem1  42344  dirkerper  42366  dirkertrigeqlem1  42368  dirkertrigeqlem3  42370  dirkertrigeq  42371  dirkeritg  42372  dirkercncflem1  42373  dirkercncflem2  42374  fourierdlem36  42413  fourierdlem41  42418  fourierdlem42  42419  fourierdlem48  42424  fourierdlem56  42432  fourierdlem57  42433  fourierdlem58  42434  fourierdlem60  42436  fourierdlem61  42437  fourierdlem62  42438  fourierdlem65  42441  fourierdlem73  42449  fourierdlem80  42456  fourierdlem87  42463  fourierdlem89  42465  fourierdlem90  42466  fourierdlem91  42467  fourierdlem100  42476  fourierdlem103  42479  fourierdlem107  42483  fourierdlem112  42488  fourierdlem113  42489  fourierdlem115  42491  fouriercnp  42496  sqwvfoura  42498  sqwvfourb  42499  fourierswlem  42500  fouriersw  42501  etransclem2  42506  etransclem37  42541  etransclem46  42550  hoidmvlelem3  42864  vonioolem2  42948  issmflem  42989  smfmullem2  43052  simpcntrab  43112  1t10e1p1e11  43495  fmtno0  43687  fmtno1  43688  fmtnorec2lem  43689  fmtnorec3  43695  fmtno2  43697  fmtno3  43698  fmtno4  43699  fmtno4sqrt  43718  fmtno4prmfac  43719  2exp5  43740  139prmALT  43744  31prm  43745  2exp7  43747  2exp11  43750  mod42tp1mod8  43752  lighneallem2  43756  5tcu2e40  43765  3exp4mod41  43766  41prothprmlem1  43767  41prothprmlem2  43768  41prothprm  43769  bits0ALTV  43829  fppr2odd  43881  341fppr2  43884  4fppr1  43885  9fppr8  43887  sbgoldbo  43937  nnsum3primes4  43938  nnsum3primesgbe  43942  nnsum4primesodd  43946  nnsum4primesoddALTV  43947  nnsum4primeseven  43950  nnsum4primesevenALTV  43951  bgoldbtbndlem1  43955  tgoldbachlt  43966  2t6m3t4e0  44381  zlmodzxzequa  44536  zlmodzxznm  44537  zlmodzxzequap  44539  nn0sumshdiglemA  44664  nn0sumshdiglemB  44665  nn0sumshdiglem1  44666  prelrrx2  44685  prelrrx2b  44686  2sphere  44721  line2  44724  itsclquadb  44748  itscnhlinecirc02plem3  44756  inlinecirc02p  44759  sec0  44844  amgmw2d  44890
  Copyright terms: Public domain W3C validator