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

Theorem eqeltri 2505
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1  |-  A  =  B
eqeltr.2  |-  B  e.  C
Assertion
Ref Expression
eqeltri  |-  A  e.  C

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2  |-  B  e.  C
2 eqeltr.1 . . 3  |-  A  =  B
32eleq1i 2498 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 201 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eqeltrri  2506  3eltr4i  2514  intab  4072  inex2  4337  pwex  4374  ord3ex  4381  zfpair  4393  opex  4419  otex  4420  uniopel  4452  tpex  4699  unisn2  4702  elvvuni  4929  isarep2  5524  fvex  5733  abrexex2  5992  ovex  6097  oprabex  6178  oprabrexex2  6180  riotaex  6544  tfrlem16  6645  1on  6722  2on  6723  3on  6725  4on  6726  oesuclem  6760  oecl  6772  nnecl  6847  1onn  6873  2onn  6874  3onn  6875  4onn  6876  mapsnf1o2  7052  map1  7176  sbthlem10  7217  map2xp  7268  nnunifi  7349  xpfi  7369  prfi  7372  tpfi  7373  fnfi  7375  pwfi  7393  inf0  7565  cantnffval  7607  cantnfvalf  7609  oemapwe  7639  cantnffval2  7640  cnfcom2  7648  cnfcom3lem  7649  cnfcom3  7650  cnfcom3clem  7651  r1fin  7688  hta  7810  infxpenlem  7884  alephon  7939  alephfplem1  7974  dfac5lem4  7996  dfac5lem5  7997  kmlem10  8028  fin1a2lem10  8278  fin1a2lem12  8280  hsmexlem9  8294  axcc2lem  8305  domtriomlem  8311  axdc2lem  8317  axcclem  8326  brdom7disj  8398  brdom6disj  8399  iundom2g  8404  konigthlem  8432  canthwelem  8514  wunex2  8602  wunex3  8605  nqex  8789  1nq  8794  1pr  8881  axcnex  9011  ax1cn  9013  negex  9293  inelr  9979  cju  9985  nnexALT  9991  2re  10058  3re  10060  4re  10062  5re  10064  6re  10065  7re  10066  8re  10067  9re  10068  10re  10069  2nn  10122  3nn  10123  4nn  10124  5nn  10125  6nn  10126  7nn  10127  8nn  10128  9nn  10129  10nn  10130  nn0ex  10216  zexALT  10289  nneo  10342  zeo  10344  decex  10373  decnncl  10384  deccl  10385  numnncl2  10388  decnncl2  10389  numsucc  10397  numma2c  10404  numadd  10405  numaddc  10406  nummul1c  10407  nummul2c  10408  qexALT  10578  xrex  10598  pnfxr  10702  mnfxr  10703  xnegex  10783  xnegcl  10788  ixxssxr  10917  om2uzuzi  11277  ltweuz  11289  axdc4uzlem  11309  seqex  11313  m1expcl2  11391  faccl  11564  facwordi  11568  faclbnd2  11570  bccl  11601  hashrabrsn  11636  hashunlei  11672  hashpw  11687  s1cli  11745  cats1un  11778  revs1  11785  cats1cli  11809  cats1fvn  11810  crre  11907  remim  11910  climmpt  12353  climle  12421  climsup  12451  sumex  12469  iserabs  12582  isumshft  12607  supcvg  12623  explecnv  12632  geo2lim  12640  ere  12679  eftlub  12698  efsep  12699  tan0  12740  ef01bndlem  12773  divalglem5  12905  divalglem9  12909  sadcf  12953  smupf  12978  crt  13155  phimullem  13156  eulerthlem2  13159  pczpre  13209  pockthi  13263  prmreclem2  13273  igz  13290  0ramcl  13379  1259lem1  13438  1259lem2  13439  1259lem3  13440  1259lem4  13441  1259lem5  13442  1259prm  13443  2503lem1  13444  2503lem2  13445  2503lem3  13446  2503prm  13447  4001lem1  13448  4001lem2  13449  4001lem3  13450  4001lem4  13451  4001prm  13452  ndxarg  13477  ressbas  13507  ressbas2  13508  ressid  13512  strle1  13548  topnid  13651  prdsbasex  13662  prdsplusg  13669  prdsmulr  13670  prdsvsca  13671  prdsle  13672  prdsds  13674  prdshom  13677  prdsco  13678  pwselbasb  13698  pwsvscafval  13704  pwssca  13706  pwssnf1o  13708  imassca  13733  imasvsca  13734  imasle  13736  xpslem  13786  xpssca  13791  xpsvsca  13792  isacs2  13866  cidfval  13889  homffval  13905  comfffval  13912  oppchomfval  13928  oppccofval  13930  oppccatid  13933  monfval  13946  oppcmon  13952  sectffval  13964  invffval  13971  isoval  13978  rescbas  14017  reschom  14018  rescco  14020  subccatid  14031  fullsubc  14035  isfunc  14049  isfuncd  14050  idfu2nd  14062  idfu1st  14064  cofu1st  14068  cofu2nd  14070  funcres2c  14086  ressffth  14123  fuccofval  14144  fuchom  14146  fucco  14147  fuccatid  14154  fucid  14156  invfuc  14159  homafval  14172  arwval  14186  idafval  14200  coafval  14207  coapm  14214  setccatid  14227  catchomfval  14241  catccofval  14243  catccatid  14245  xpcbas  14263  xpchomfval  14264  xpccofval  14267  xpccatid  14273  1stf1  14277  1stf2  14278  2ndf1  14280  2ndf2  14281  prf1  14285  prf2fval  14286  evlf2  14303  evlf1  14305  curf1fval  14309  curf11  14311  curf12  14312  curf1cl  14313  curf2  14314  curf2cl  14316  hof2fval  14340  yonedalem4a  14360  yonedalem4c  14362  yonedalem3  14365  yonedainv  14366  isdrs  14379  ispos  14392  isposix  14402  pltfval  14404  lubfval  14423  lubval  14424  lubprop  14425  glbfval  14428  glbval  14429  glbprop  14430  joinfval  14432  joinlem  14435  meetfval  14439  meetlem  14442  clatlem  14527  isglbd  14532  odupos  14550  oduglb  14554  odumeet  14555  odulub  14556  odujoin  14557  ipolt  14573  ipopos  14574  isacs4lem  14582  isdlat  14607  plusffval  14690  issubmnd  14712  ismhm  14728  0mhm  14746  submacs  14753  pwsdiagmhm  14756  gsumvalx  14762  gsumval  14763  gsumress  14765  gsumz  14769  frmdplusg  14787  grpinvfval  14831  grpsubfval  14835  grplactfval  14873  mulgfval  14879  mulgval  14880  issubg  14932  0subg  14953  subgacs  14963  nsgacs  14964  nmznsg  14972  eqgfval  14976  eqgen  14981  isghm  14994  gicen  15052  isga  15056  subgga  15065  orbstafun  15076  orbstaval  15077  orbsta  15078  orbsta2  15079  symgplusg  15087  cayleylem2  15099  cntzfval  15107  cntzval  15108  oppgplusfval  15132  odfval  15159  odval  15160  odinf  15187  dfod2  15188  pgpfi1  15217  pgp0  15218  sylow1lem2  15221  sylow2alem2  15240  sylow2blem1  15242  sylow2blem2  15243  sylow3lem6  15254  lsmfval  15260  lsmvalx  15261  oppglsm  15264  pj1fval  15314  efglem  15336  efgtf  15342  efgsval2  15353  efgsp1  15357  efgrelexlemb  15370  efgcpbllemb  15375  frgpeccl  15381  frgpmhm  15385  vrgpval  15387  frgpuplem  15392  frgpupf  15393  frgpupval  15394  frgpup1  15395  frgpup3lem  15397  frgpnabllem1  15472  frgpnabllem2  15473  iscygodd  15486  prmcyg  15491  lt6abl  15492  dprdfeq0  15568  dmdprdsplitlem  15583  ablfacrplem  15611  ablfacrp  15612  ablfacrp2  15613  ablfac1a  15615  ablfac1b  15616  ablfac1c  15617  ablfac1eu  15619  pgpfaclem2  15628  ablfaclem1  15631  ablfaclem2  15632  ablfaclem3  15633  mgpplusg  15640  mgpress  15647  pwsmgp  15712  opprmulfval  15718  dvdsrval  15738  isunit  15750  unitgrp  15760  unitlinv  15770  unitrinv  15771  dvrfval  15777  isirred  15792  isdrng2  15833  drngmcl  15836  drngid2  15839  issubrg  15856  subrgugrp  15875  isabv  15895  staffval  15923  islmod  15942  scaffval  15956  lssset  15998  islss  15999  lsssn0  16012  lssacs  16031  lspfval  16037  lspval  16039  lspcl  16040  lspuni0  16074  lss0v  16080  0lmhm  16104  lmhmvsca  16109  islbs  16136  islbs3  16215  lbsextlem1  16218  lbsextlem3  16220  lbsextlem4  16221  lbsext  16223  rsp1  16283  drngnidl  16288  2idlval  16292  divsrhm  16296  isnzr2  16322  rrgval  16335  aspval  16375  asclfval  16381  gsumbagdiag  16429  psrbas  16431  psrelbas  16432  psrplusg  16433  psrmulr  16436  psrmulfval  16437  psrmulcllem  16439  psrvscafval  16442  psrvscaval  16444  psrvscacl  16445  psr0cl  16446  psr0lid  16447  psrnegcl  16448  psrlinv  16449  psr1cl  16454  psrlidm  16455  psrridm  16456  psrdi  16458  psrdir  16459  psrass23  16461  resspsradd  16467  resspsrmul  16468  resspsrvsca  16469  mvrval  16473  mvrval2  16474  mplsubglem  16486  mpladd  16493  mplmul  16494  mplvscaval  16499  ressmpladd  16508  ressmplmul  16509  ressmplvsca  16510  subrgmvr  16512  mplmon  16514  mplmonmul  16515  mplcoe1  16516  ltbval  16520  opsrle  16524  opsrtoslem2  16533  mplmon2  16541  psrbag0  16542  psrbagsn  16543  subrgascl  16546  evlslem2  16556  psr1baslem  16571  ressply1add  16612  ressply1mul  16613  ressply1vsca  16614  psropprmul  16620  coe1tmmul2fv  16658  coe1pwmulfv  16660  ply1coe  16672  xrsex  16704  expghm  16765  zrhrhmb  16780  zlmlem  16786  zlmsca  16790  zlmvsca  16791  znle  16805  znbas  16812  znzrhval  16815  zntoslem  16825  znfi  16828  znidomb  16830  znunithash  16833  ipffval  16867  ocvfval  16881  ocvval  16882  elocv  16883  thlbas  16911  thlle  16912  thlleval  16913  thloc  16914  pjfval  16921  pjdm  16922  pjpm  16923  isobs  16935  indistopon  17053  iccordt  17266  concompid  17482  ptbasfi  17601  imastopn  17740  ptcmpfi  17833  uzrest  17917  tmdgsum2  18114  distgp  18117  indistgp  18118  cldsubg  18128  snclseqg  18133  tsmsval  18148  tsmsadd  18164  ustfn  18219  ust0  18237  ustn0  18238  ussid  18278  isusp  18279  ressust  18282  cnextucn  18321  prdsxmetlem  18386  tmslem  18500  nrmmetd  18610  nmfval  18624  tnglem  18669  tngds  18677  tngnm  18680  tngngp2  18681  tngngpd  18682  tngngp  18683  nghmfval  18744  nmo0  18757  cnbl0  18796  remet  18809  re2ndc  18820  xrrest  18826  zcld  18832  icccmp  18844  xrge0gsumle  18852  xrge0tsms  18853  xmetdcn  18857  divcn  18886  expcn  18890  iicon  18905  climcncf  18918  cnmpt2pc  18941  cnrehmeo  18966  cnheiborlem  18967  rellycmp  18970  bndth  18971  evth2  18973  pi1bas  19051  cphsubrglem  19128  cphcjcl  19134  tchex  19164  ipcau2  19179  cncmet  19263  cmsss  19291  ishl2  19312  minveclem4a  19319  minveclem4  19321  finiunmbl  19426  ioombl1lem4  19443  vitalilem4  19491  vitalilem5  19492  ismbf2d  19521  mbfimaopnlem  19535  mbflimsup  19546  mbflim  19548  mbfi1fseqlem6  19600  itgex  19650  bddmulibl  19718  ditgex  19727  recnperf  19780  dv11cn  19873  dvcnvrelem2  19890  ftc1  19914  evlslem3  19923  evlslem1  19924  evlsval2  19929  evl1fval  19935  evl1val  19936  evl1rhm  19937  evl1sca  19938  evl1var  19940  evl1addd  19942  evl1subd  19943  evl1muld  19944  evl1expd  19946  pf1f  19958  pf1mpf  19960  pf1ind  19963  mdegfval  19973  mdegldg  19977  mdegcl  19980  mdegmullem  19989  uc1pval  20050  mon1pval  20052  q1pval  20064  r1pval  20067  ply1remlem  20073  ply1rem  20074  facth1  20075  fta1glem1  20076  fta1glem2  20077  fta1blem  20079  ig1pval  20083  plyeq0lem  20117  quotval  20197  elqaalem3  20226  aaliou3lem4  20251  ulmcau  20299  ulmdvlem1  20304  ulmdvlem3  20306  mbfulm  20310  itgulm  20312  dvradcnv  20325  pserdvlem2  20332  sincn  20348  coscn  20349  tanabsge  20402  reloggim  20481  logcn  20526  dvloglem  20527  logdmopn  20528  dvlog2  20532  cxpcn  20617  cxpcn3  20620  resqrcn  20621  ang180lem3  20641  atanrecl  20739  atan1  20756  atansopn  20760  birthdaylem1  20778  birthday  20781  emcllem4  20825  emcllem6  20827  basellem6  20856  ppiublem1  20974  dchrplusg  21019  dchrmulid2  21024  dchrinvcl  21025  dchrptlem2  21037  dchrsum2  21040  sumdchr2  21042  dchr2sum  21045  bposlem6  21061  bposlem8  21063  lgslem4  21071  lgsdir2lem2  21096  selberglem1  21227  selberglem3  21229  selberg  21230  selbergs  21256  qdrng  21302  usgraexmpl  21408  nbgraf1o0  21444  wlkntrl  21550  0pth  21558  constr1trl  21576  constr2wlk  21586  constr2trl  21587  constr2spth  21588  constr2pth  21589  constr3lem1  21620  constr3trllem3  21627  eupatrl  21678  eupath  21691  konigsberg  21697  gxval  21834  issubgoi  21886  rngoi  21956  dvrunz  22009  isvci  22049  isnvi  22080  imsmetlem  22170  dipfval  22186  sspval  22210  islno  22242  nmooval  22252  nmounbseqi  22266  nmobndseqi  22268  bloval  22270  0ofval  22276  0oval  22277  blocni  22294  ajfval  22298  hmoval  22299  cncph  22308  isph  22311  phpar  22313  ipasslem7  22325  siilem2  22341  ajval  22351  ubthlem1  22360  ubthlem2  22361  minvecolem4b  22368  minvecolem4  22370  minvecolem5  22371  hlex  22388  normlem2  22601  normlem3  22602  normlem6  22605  h0elch  22745  hhsssh  22757  spansnji  23136  nonbooli  23141  3oalem5  23156  3oalem6  23157  3oai  23158  mayetes3i  23220  nmcexi  23517  nmbdfnlb  23541  rnelshi  23550  cnlnadjlem5  23562  pjbdlni  23640  golem2  23763  goeqi  23764  ress0g  24170  ressplusf  24171  ressnm  24172  xrge0tsmsd  24211  rdivmuldivd  24215  rnginvval  24216  dvrcan5  24217  ofldlt1  24231  inftmrel  24238  isinftm  24239  relt  24264  redvr  24265  retos  24266  refld  24267  pstmfval  24279  tpr2tp  24290  tpr2rico  24298  mndpluscn  24300  xrge0pluscn  24314  xrge0mulc1cn  24315  xrge0haus  24318  lmlimxrge0  24322  lmxrge0  24325  qqhval  24346  qqhcn  24363  qqhucn  24364  esumex  24414  esumcst  24443  hasheuni  24463  esumcvg  24464  isrnsigaOLD  24483  prsiga  24502  brsiga  24525  mbfmcnt  24606  sxbrsigalem3  24610  dya2iocuni  24621  dya2iocucvr  24622  sxbrsigalem1  24623  sxbrsiga  24628  sibf0  24637  sibfof  24642  sitgclg  24644  coinflipprob  24725  coinfliprv  24728  lgamgulmlem5  24805  lgamgulmlem6  24806  lgamgulm2  24808  lgamcvglem  24812  subfacp1lem1  24853  subfacp1lem3  24856  subfacp1lem5  24858  subfacp1lem6  24859  kur14lem7  24886  iiscon  24927  iillyscon  24928  cvmliftlem5  24964  cvmliftlem8  24967  cvmliftlem10  24969  cvmlift2lem9  24986  ghomgrpilem2  25085  ghomsn  25087  ghomgrplem  25088  circum  25099  climlec3  25202  prodfclim1  25210  prodex  25222  predasetex  25435  trpredex  25495  altopex  25753  colinearex  25942  bpoly4  26053  rankeq1o  26060  ssoninhaus  26146  areacirc  26234  upixp  26368  sdclem2  26383  sdclem1  26384  fdc  26386  lmclim2  26401  caures  26403  idcncf  26406  cncfres  26411  heibor1lem  26455  heiborlem3  26459  heibor  26467  rrnval  26473  rrnmet  26475  reheibor  26485  grpokerinj  26497  isdrngo1  26509  isdrngo2  26511  isrngohom  26518  idlval  26560  isidl  26561  0idl  26572  0rngo  26574  divrngidl  26575  smprngopr  26599  igenval  26608  mapfzcons2  26712  jm2.23  27004  jm2.27dlem2  27018  jm2.27dlem4  27020  rmydioph  27022  rmxdioph  27024  expdiophlem2  27030  expdioph  27031  aomclem6  27071  islssfgi  27085  pwssplit4  27106  pwslnmlem0  27108  frlmbas  27138  frlmbasf  27143  frlmvscafval  27145  uvcvval  27150  uvcvvcl  27151  frlmsslss2  27160  frlmlbs  27164  ellspd  27169  elfilspd  27170  mapfien2  27173  pwfi2en  27176  frlmpwfi  27177  islinds2  27198  lsslindf  27215  lsslinds  27216  islindf4  27223  hbtlem1  27242  hbtlem7  27244  mncn0  27259  aaitgo  27282  symgfisg  27324  psgnfval  27338  cnmsgnsubg  27349  psgnghm  27352  psgnghm2  27353  mndvcl  27361  mamucl  27371  mamudiagcl  27372  mamulid  27373  mamurid  27374  mamuvs1  27378  mamuvs2  27379  matmulr  27382  mdetfval  27402  mendplusgfval  27408  mendmulrfval  27410  mendvscafval  27413  subrgacs  27423  sdrgacs  27424  cntzsdrg  27425  idomrootle  27426  idomodle  27427  deg1mhm  27441  rfcnpre1  27604  fcnre  27610  refsumcn  27615  refsum2cnlem1  27622  clim1fr1  27641  climexp  27645  climinf  27646  climneg  27650  climdivf  27652  itgsin0pilem1  27658  stoweidlem47  27710  stoweidlem53  27716  stoweidlem57  27720  stoweidlem59  27722  wallispilem3  27730  wallispilem4  27731  wallispilem5  27732  wallispi  27733  stirlinglem1  27737  stirlinglem8  27744  stirlinglem12  27748  stirlinglem13  27749  stirlinglem14  27750  stirlinglem15  27751  usgra2adedgwlkon  28191  dpval  28371  bnj105  28943  bnj918  28989  bnj95  29089  bnj852  29146  bnj865  29148  lshpset  29615  lsatset  29627  lcvfbr  29657  islfl  29697  lfl0f  29706  lfl1  29707  lfladd0l  29711  lflnegl  29713  lflvscl  29714  lflvsdi1  29715  lflvsdi2  29716  lflvsdi2a  29717  lflvsass  29718  lfl0sc  29719  lflsc0N  29720  lfl1sc  29721  lkrfval  29724  lkr0f  29731  lkrsc  29734  eqlkr2  29737  ldualvbase  29763  ldualfvadd  29765  ldualvaddval  29768  ldualsca  29769  ldualfvs  29773  ldualvsval  29775  isopos  29817  cmtfvalN  29847  cvrfval  29905  pats  29922  glbconN  30013  llnset  30141  lplnset  30165  lvolset  30208  lineset  30374  isline  30375  pointsetN  30377  psubspset  30380  ispsubsp  30381  pmapfval  30392  pmapval  30393  paddfval  30433  paddval  30434  pclfvalN  30525  pclvalN  30526  polfvalN  30540  polvalN  30541  psubclsetN  30572  ispsubclN  30573  watfvalN  30628  watvalN  30629  lhpset  30631  lautset  30718  islaut  30719  pautsetN  30734  ispautN  30735  ldilfset  30744  ldilset  30745  ltrnfset  30753  ltrnset  30754  dilfsetN  30788  dilsetN  30789  trnfsetN  30791  trlfset  30796  cdleme25cl  30993  cdleme26e  30995  cdleme26eALTN  30997  cdleme26fALTN  30998  cdleme26f  30999  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme29cl  31013  cdleme31snd  31022  cdleme31fv  31026  cdlemefrs29clN  31035  cdlemefs32sn1aw  31050  cdleme43fsv1snlem  31056  cdleme41sn3a  31069  cdleme32a  31077  cdleme40m  31103  cdleme40n  31104  cdleme42b  31114  cdlemeg46c  31149  tgrpfset  31380  tgrpbase  31382  tgrpopr  31383  tendofset  31394  istendo  31396  tendopl  31412  tendo02  31423  tendoi  31430  erngfset  31435  erngbase  31437  erngfplus  31438  erngfmul  31441  erngfset-rN  31443  erngbase-rN  31445  erngfplus-rN  31446  erngfmul-rN  31449  cdlemk29-3  31547  cdlemk36  31549  cdlemk40  31553  cdlemkid5  31571  cdlemkid  31572  cdlemk56  31607  dvafset  31640  dvasca  31642  dvavbase  31649  dvafvadd  31650  dvafvsca  31652  diaffval  31667  diafval  31668  diaval  31669  dvhfset  31717  dvhsca  31719  dvhvbase  31724  dvhfvadd  31728  dvhfvsca  31737  docaffvalN  31758  docafvalN  31759  docavalN  31760  djaffvalN  31770  djafvalN  31771  djavalN  31772  dibffval  31777  dibfval  31778  dibopelvalN  31780  dibopelval2  31782  dibelval3  31784  diblsmopel  31808  dicffval  31811  dicfval  31812  dicval  31813  cdlemn11a  31844  dihffval  31867  dihfval  31868  dihvalcqpre  31872  dihopelvalcpre  31885  dihord6apre  31893  dihpN  31973  dochffval  31986  dochfval  31987  dochval  31988  djhffval  32033  djhfval  32034  djhval  32035  islpolN  32120  lpolconN  32124  dochpolN  32127  lcfrlem8  32186  lcfrlem9  32187  lcdfval  32225  lcd0vvalN  32250  mapdffval  32263  mapdfval  32264  mapdval  32265  mapd1o  32285  mapdunirnN  32287  mapdhval  32361  mapdhval0  32362  hvmapffval  32395  hvmapfval  32396  hvmapval  32397  hdmap1ffval  32433  hdmap1fval  32434  hdmap1vallem  32435  hdmapffval  32466  hdmapfval  32467  hgmapffval  32525  hgmapfval  32526  hlhilset  32574  hlhilsca  32575  hlhilbase  32576  hlhilplus  32577  hlhilvsca  32587  hlhilip  32588  hlhilnvl  32590  hlhillsm  32596  hlhillcs  32598
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator