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

Theorem eleq2d 2502
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq2d  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2d
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq2 2496 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleq12d  2503  eleqtrd  2511  neleqtrd  2530  neleqtrrd  2531  abeq2d  2544  nfceqdf  2570  drnfc1  2587  drnfc2  2588  sbcbid  3206  cbvcsb  3247  sbcel1g  3262  csbeq2d  3267  csbie2g  3289  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  cbviun  4120  cbviin  4121  iinxsng  4159  iinxprg  4160  iunxsng  4161  cbvdisj  4184  disjor  4188  mpteq12f  4277  axpweq  4368  rabxfrd  4736  0nelelxp  4899  opeliunxp  4921  opeliunxp2  5005  iunxpf  5013  elrelimasn  5220  elimasng  5222  elimasni  5223  ressn  5400  funfni  5537  fnbr  5539  fun11iun  5687  dffv3  5716  fvelrnb  5766  fvun1  5786  fvco2  5790  elpreima  5842  dff3  5874  fmptco  5893  fnpr  5942  fnprOLD  5943  zfrep6  5960  funfvima3  5967  eluniima  5989  dff13  5996  f1eqcocnv  6020  isoini  6050  mpt2eq123dva  6127  cbvmpt2x  6142  ovelrn  6214  elovmpt2  6283  fmpt2x  6409  bropopvvv  6418  mpt2xopn0yelv  6456  mpt2xopovel  6463  isprmpt2  6469  rntpos  6484  riotaeqdv  6542  onoviun  6597  smoel  6614  smoiso  6616  smoel2  6617  smo11  6618  tfrlem9  6638  oalimcl  6795  oaass  6796  omordi  6801  omordlim  6812  omlimcl  6813  odi  6814  omeulem1  6817  omeulem2  6818  oen0  6821  oeordi  6822  oeordsuc  6829  oelimcl  6835  oeeulem  6836  oeeui  6837  nnmordi  6866  oaabs2  6880  omabs  6882  omsmolem  6888  ereldm  6940  iiner  6968  elmapg  7023  elpmg  7024  elixpsn  7093  ixpsnf1o  7094  boxriin  7096  omxpenlem  7201  pw2f1olem  7204  phplem4  7281  php3  7285  elfi  7410  dffi3  7428  marypha2lem2  7433  ordiso2  7476  wemapso2lem  7511  elharval  7523  inf3lemd  7574  inf3lem1  7575  inf3lem2  7576  inf3lem3  7577  cantnfs  7613  cantnfp1lem3  7628  cantnflem1b  7634  cantnflem1  7637  trcl  7656  r1sdom  7692  r1ordg  7696  r1pwss  7702  tz9.12lem3  7707  tz9.12  7708  r1elwf  7714  rankr1ai  7716  rankidb  7718  rankr1bg  7721  rankval2  7736  rankunb  7768  tcrank  7800  fseqdom  7899  acni  7918  acni2  7919  acndom  7924  infpwfien  7935  alephnbtwn  7944  cardaleph  7962  cardinfima  7970  iunfictbso  7987  dfac3  7994  dfac5lem5  8000  dfac5  8001  dfac9  8008  dfac12r  8018  kmlem2  8023  kmlem12  8033  kmlem13  8034  kmlem14  8035  ackbij2lem3  8113  ackbij2  8115  cofsmo  8141  cfsmolem  8142  alephsing  8148  fin23lem30  8214  isf32lem9  8233  itunisuc  8291  axcc2lem  8308  axcc3  8310  domtriomlem  8314  axdc2lem  8320  axdc2  8321  axdc3lem2  8323  axdc3lem4  8325  axdc4lem  8327  ac6c4  8353  zorn2lem1  8368  ttukeylem6  8386  pwcfsdom  8450  axregndlem2  8470  axinfndlem1  8472  axacndlem4  8477  axacnd  8479  pwfseqlem1  8525  inar1  8642  inatsk  8645  gruurn  8665  grur1  8687  grothpw  8693  eltskm  8710  genpelv  8869  eluz1  10484  eluzadd  10506  eluzsub  10507  elixx1  10917  elixx3g  10921  elioo2  10949  elfz1  11040  elfz2  11042  elfzp1  11089  fzpr  11093  fzsuc2  11096  fzrev3  11103  elfzp12  11118  elfzo  11134  elfzom1b  11183  fzosplitsni  11188  seqp1  11330  seqf1o  11356  bcval  11587  bcpasc  11604  hashf1lem1  11696  ccatfval  11734  ccatlid  11740  ccatass  11742  swrdid  11764  ccatswrd  11765  swrdccat2  11767  cats1un  11782  revccat  11790  revrev  11791  revco  11795  ccatco  11796  shftfn  11880  shftval  11881  limsupgle  12263  ello12  12302  elo12  12313  isercolllem3  12452  sumeq1f  12474  fsumsplit  12525  sumsplit  12544  fsum2dlem  12546  fsumcom2  12550  fsumparts  12577  explecnv  12636  eftlub  12702  divalgmod  12918  bitsval  12928  bitsp1e  12936  bitsp1o  12937  sadfval  12956  sadcp1  12959  sadval  12960  sadcadd  12962  sadadd2  12964  saddisjlem  12968  sadadd  12971  sadass  12975  smufval  12981  smuval  12985  smuval2  12986  smupvallem  12987  smu01lem  12989  smueqlem  12994  smumul  12997  bezoutlem2  13031  bezoutlem4  13033  algfx  13063  eucalgcvga  13069  unbenlem  13268  prmreclem5  13280  vdwapval  13333  vdwapun  13334  vdwnnlem1  13355  vdwnn  13358  ramval  13368  0ram  13380  ramub1lem2  13387  prmlem0  13420  elrest  13647  prdsbasmpt  13684  prdsleval  13691  prdsbasmpt2  13696  pwselbasb  13702  imasaddfnlem  13745  imasvscafn  13754  divsfval  13764  ismre  13807  mreunirn  13818  mrisval  13847  ismri  13848  isacs  13868  catidd  13897  iscatd2  13898  ismon  13951  isepi  13958  sectffval  13968  sectfval  13969  issubc  14027  isfunc  14053  funcres  14085  funcpropd  14089  ffthiso  14118  isnat  14136  isnat2  14137  fuciso  14164  arwhoma  14192  elsetchom  14228  setcmon  14234  setcepi  14235  setciso  14238  catciso  14254  hofcl  14348  hofpropd  14356  yonedalem4c  14366  yonedainv  14370  yonffthlem  14371  poslubdg  14567  acsficl2d  14594  acsmapd  14596  psref  14632  psss  14638  dirge  14674  grpidval  14699  grpidd  14710  ismndd  14711  mndpropd  14713  grpidpropd  14714  imasmnd2  14724  imasmnd  14725  ismhm  14732  issubm  14740  gsumccat  14779  imasgrp2  14925  imasgrp  14926  issubg  14936  subginv  14943  isnsg  14961  isghm  14998  resghm2b  15016  conjnmzb  15032  conjnsg  15033  ghmpropd  15035  isga  15060  elcntz  15113  elcntzsn  15116  cntzrcl  15118  resscntz  15122  gexdvds  15210  gex1  15217  isslw  15234  sylow3lem2  15254  lsmelvalx  15266  pj1ghm  15327  efgtlen  15350  efgs1b  15360  efgsfo  15363  efgredlemc  15369  frgp0  15384  frgpmhm  15389  divsabl  15472  frgpnabllem1  15476  0cyg  15494  cycsubgcyg  15502  gsumval3  15506  gsumcllem  15508  gsumzaddlem  15518  gsumzsplit  15521  eldprd  15554  dprdcntz2  15588  dprd2d2  15594  dmdprdsplit2lem  15595  dmdprdsplit2  15596  dprdsplit  15598  ablfac2  15639  isrngd  15690  imasrng  15717  dvdsrval  15742  isunit  15754  dvdsrpropd  15793  isirred  15796  isrhm  15816  drngunit  15832  isdrngd  15852  issubrg  15860  opprsubrg  15881  rhmpropd  15895  isabv  15899  issrngd  15941  islmod  15946  lmodprop2d  15998  islss  16003  islssd  16004  lssats2  16068  lspsnel  16071  islmhm  16095  lmhmf1o  16114  lmhmima  16115  lmhmpreima  16116  reslmhm  16120  lmhmpropd  16137  islbs  16140  lspprel  16158  lspfixed  16192  lbsacsbs  16220  lbsextlem1  16222  lbsextlem2  16223  lbsextlem3  16224  lbsextlem4  16225  lidlmcl  16280  divscrng  16303  islpidl  16309  lidldvgen  16318  mplsubglem  16490  mpllsslem  16491  mplmonmul  16519  mplrcl  16542  subrgascl  16550  subrgasclcl  16551  strov2rcl  16623  zrhrhmb  16784  znf1o  16824  frgpcyg  16846  isphld  16877  elocv  16887  iscss  16902  isobs  16939  obs2ss  16948  istopon  16982  eltg  17014  eltg2  17015  eltop  17031  eltop2  17032  eltop3  17033  pptbas  17064  iscld  17083  neiss2  17157  isnei  17159  neiptopnei  17188  neiptopreu  17189  lpfval  17194  lpval  17195  islp  17196  maxlp  17203  islpi  17205  neitr  17236  restlp  17239  ordtbas2  17247  ordtrest2  17260  lmfval  17288  cnfval  17289  iscn  17291  iscnp  17293  tgcn  17308  tgcnp  17309  lmbrf  17316  cnpresti  17344  ist1  17377  ist1-2  17403  cnt1  17406  haust1  17408  cmpfi  17463  cmpfii  17464  1stcfb  17500  2ndc1stc  17506  1stcrest  17508  2ndcdisj  17511  1stcelcls  17516  nllyi  17530  subislly  17536  kgenval  17559  elkgen  17560  kgencn2  17581  txbas  17591  eltx  17592  ptval  17594  ptpjpre1  17595  ptopn2  17608  ptpjopn  17636  ptclsg  17639  xkoccn  17643  txdis  17656  txdis1cn  17659  ptrescn  17663  hausdiag  17669  hauseqlcld  17670  txhaus  17671  xkohaus  17677  elqtop  17721  qtopeu  17740  kqcldsat  17757  hmeofval  17782  ptuncnv  17831  ptunhmeo  17832  elmptrab  17851  fbdmn0  17858  elfg  17895  elfilss  17900  filunirn  17906  fixufil  17946  elfm  17971  rnelfmlem  17976  rnelfm  17977  fmfnfmlem4  17981  elflim2  17988  flimtopon  17994  elflim  17995  hausflim  18005  flimcls  18009  flfnei  18015  isflf  18017  hausflf  18021  cnpflf  18025  cnflf  18026  txflf  18030  isfcls  18033  fclstopon  18036  isfcls2  18037  fclssscls  18042  fclsnei  18043  fclsfnflim  18051  flimfnfcls  18052  isfcf  18058  fcfelbas  18060  cnpfcf  18065  cnfcf  18066  alexsublem  18067  alexsubALTlem3  18072  cnextfun  18087  cnextfvval  18088  cnextf  18089  cnextcn  18090  tmdgsum2  18118  tgpconcomp  18134  ghmcnp  18136  divstgplem  18142  eltsms  18154  haustsms  18157  tsmsgsum  18160  tsmssubm  18164  tsmssplit  18173  isust  18225  elrnust  18246  ustbas  18249  elutop  18255  ustuqtoplem  18261  ustuqtop4  18266  ustuqtop  18268  utopsnneiplem  18269  utopsnneip  18270  utopsnnei  18271  isusp  18283  isucn  18300  ucncn  18307  iscfilu  18310  neipcfilu  18318  iscusp  18321  cnextucn  18325  ispsmet  18327  ismet  18345  isxmet  18346  elblps  18409  elbl  18410  elmopn  18464  prdsbl  18513  neibl  18523  met1stc  18543  metrest  18546  prdsxmslem2  18551  txmetcnp  18569  txmetcn  18570  metuvalOLD  18571  metuval  18572  metustsymOLD  18583  metustsym  18584  cfilucfil2OLD  18595  cfilucfil2  18596  elbl4  18598  metuelOLD  18599  metuel  18600  metutopOLD  18604  psmetutop  18605  restmetu  18609  metucnOLD  18610  metucn  18611  tngngp  18687  isnmhm  18772  zcld  18836  metnrmlem1a  18880  elcncf  18911  cncfcnvcn  18943  cnheibor  18972  lebnumlem1  18978  ishtpy  18989  isphtpy  18998  om1elbas  19049  elpi1  19062  pi1xfr  19072  pi1coghm  19078  tchcph  19186  lmmbrf  19207  iscfil  19210  iscau  19221  iscauf  19225  caucfil  19228  iscmet  19229  cmetcaulem  19233  iscmet3lem1  19236  iscmet3lem2  19237  iscmet3  19238  bcthlem1  19269  cmsss  19295  cmetcusp1OLD  19297  cmetcusp1  19298  cmetcuspOLD  19299  cmetcusp  19300  minveclem3b  19321  ovolfioo  19356  ovolficc  19357  ovolctb  19378  ovoliunnul  19395  ovolshftlem1  19397  sca2rab  19400  ovolscalem1  19401  ovolicc2lem1  19405  ovolicc2lem2  19406  ovolicc2lem4  19408  ovolicc2lem5  19409  iundisj  19434  iunmbl2  19443  uniioombllem3  19469  vitalilem2  19493  vitalilem3  19494  mbfss  19530  i1faddlem  19577  i1fmullem  19578  mbfi1fseqlem2  19600  mbfi1fseqlem4  19602  mbfi1fseq  19605  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2gt0  19644  isibl  19649  iblss2  19689  itgss3  19698  itgsplit  19719  ellimc  19752  limcmo  19761  cnlimc  19767  limciun  19773  limcun  19774  eldv  19777  dvbsss  19781  dvreslem  19788  elcpn  19812  dvaddf  19820  dvmulf  19821  dvcof  19826  rolle  19866  dvlip2  19871  dvivthlem1  19884  lhop1  19890  lhop2  19891  ftc1cn  19919  mpfind  19957  fta1glem2  20081  plyco0  20103  elply  20106  ply1termlem  20114  eltayl  20268  tayl0  20270  taylplem1  20271  taylplem2  20272  dvtaylp  20278  taylthlem1  20281  taylthlem2  20282  abelth  20349  cxpcn3  20624  rlimcnp  20796  fsumharmonic  20842  dchrelbas  21012  pntrsumbnd2  21253  ostth2lem2  21320  usgra2edg1  21395  usgraidx2vlem1  21402  usgraidx2vlem2  21403  nbgraop  21428  nbgrael  21430  nbgraeledg  21434  nbgraf1olem1  21443  nbgraf1olem3  21445  nbgraf1olem5  21447  nbgraf1o  21449  iscusgra  21457  sizeusglecusglem1  21485  isuvtx  21489  uvtxel  21490  uvtxisvtx  21491  wlks  21518  iswlk  21519  istrl  21529  ispth  21560  isspth  21561  fargshiftlem  21613  fargshiftfv  21614  fargshiftfo  21617  vdgrfval  21658  vdgrun  21664  vdgrfiun  21665  vdgr1a  21669  eupap1  21690  eupath2lem3  21693  ex-res  21741  isabloda  21879  issubgo  21883  isass  21896  elghomlem2  21942  ghablo  21949  iscom2  21992  rngoidmlem  22003  rngo1cl  22009  isssp  22215  sspn  22227  islno  22246  isblo  22275  nmlno0  22288  ishmo  22304  dipdir  22335  dipass  22338  ubthlem1  22364  ubthlem2  22365  htthlem  22412  htth  22413  ocel  22775  ocnel  22792  shsel  22808  shsel2  22816  shmodsi  22883  pjhtheu  22888  pjeq  22893  axpjpj  22914  pjoc2  22933  elspani  23037  h1de2ctlem  23049  elspansn  23060  elspansn2  23061  elnlfn  23423  eleigvec  23452  riesz3i  23557  iuneq12daf  23999  iuneq12df  24000  iunrdx  24006  cbvdisjf  24007  disjorf  24013  disjabrex  24016  disjabrexf  24017  iundisjf  24021  disjrdx  24023  elunirn2  24055  abfmpunirn  24056  abfmpeld  24058  abfmpel  24059  fmptdF  24061  fmptcof2  24068  funcnvmptOLD  24074  funcnvmpt  24075  xrofsup  24118  iundisjfi  24144  eliccioo  24169  xrge0tsmsbi  24216  inftmrel  24242  isinftm  24243  metidval  24277  pstmval  24282  cnre2csqima  24301  fmcncfil  24309  ofcfval  24473  measvuni  24560  meascnbl  24565  faeval  24589  ismbfm  24594  elunirnmbfm  24595  isanmbfm  24598  imambfm  24604  itgeq12dv  24633  issibf  24640  rrvmbfm  24692  elorvc  24709  elorrvc  24713  dstfrvunirn  24724  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsima  24765  ballotlemrv  24769  subfacp1lem2b  24859  subfacp1lem4  24861  subfacp1lem5  24862  subfacp1lem6  24863  ptpcon  24912  cvmscbv  24937  iscvm  24938  cvmsi  24944  cvmsval  24945  cvmliftmolem1  24960  cvmlift2lem12  24993  cvmlift2lem13  24994  cvmlift3lem7  25004  snmlval  25010  elgiso  25099  fprodser  25267  fprodsplit  25281  fprod2dlem  25296  fprodcom2  25300  mpteq12d  25388  opelco3  25395  predbrg  25453  trpredrec  25508  wfrlem9  25538  wfrlem12  25541  wsuclem  25568  fvnobday  25629  nodenselem3  25630  nodenselem5  25632  nofulllem5  25653  elee  25825  brbtwn  25830  brcgr  25831  axlowdimlem16  25888  funtransport  25957  fvtransport  25958  brcolinear  25985  colineardim1  25987  funray  26066  fvray  26067  funline  26068  fvline  26070  lineelsb2  26074  rankelg  26101  rankeq1o  26104  elhf2  26108  0hf  26110  mblfinlem  26234  volsupnfl  26241  itg2addnclem  26246  itg2gt0cn  26250  islocfin  26367  lfinpfin  26374  locfindis  26376  locfincf  26377  comppfsc  26378  neibastop2lem  26380  neibastop3  26382  eltail  26394  indexdom  26427  incsequz  26443  istotbnd  26469  istotbnd3  26471  0totbnd  26473  sstotbnd  26475  sstotbnd3  26476  isbnd  26480  prdstotbnd  26494  cntotbnd  26496  isismty  26501  heibor1lem  26509  heiborlem2  26512  heiborlem3  26513  heibor  26521  exidcl  26542  exidreslem  26543  divrngcl  26564  isdrngo2  26565  isrngohom  26572  isrngoiso  26585  isriscg  26591  iscringd  26600  isidl  26615  ispridl  26635  ismaxidl  26641  prter3  26722  fnelfp  26727  fnelnfp  26729  isnacs  26749  mrefg2  26752  elmzpcl  26774  mzpcompact2  26800  eldiophb  26806  elpell1qr  26901  elpell14qr  26903  elpell1234qr  26905  pw2f1ocnv  27099  pw2f1o2val2  27102  aomclem4  27123  aomclem6  27125  islssfg2  27137  pwssplit3  27158  dsmmbas2  27171  dsmmfi  27172  dsmmelbas  27173  dsmmlss  27178  frlmelbas  27192  frlmlbs  27217  frlmup1  27218  ellspd  27222  imasgim  27232  islinds  27247  islindf2  27252  f1lindf  27260  islindf4  27276  lnr2i  27288  elmnc  27309  rngunsnply  27346  f1otrspeq  27358  pmtrfrn  27368  psgnunilem1  27384  psgnunilem5  27385  psgnunilem2  27386  psgnunilem3  27387  psgneldm2  27395  mat1  27450  issdrg  27473  dvconstbi  27519  stoweidlem27  27743  stoweidlem29  27745  stoweidlem31  27747  stoweidlem34  27750  stoweidlem48  27764  stoweidlem59  27775  afvelrnb  27994  afvelrnb0  27995  ubmelfzo  28109  elfzelfzccat  28150  swrd0swrd  28163  swrdswrd  28165  swrdswrd0  28167  swrdccatfn  28170  swrdccatin1  28171  swrdccatin12lem2  28173  swrdccatin12lem3b  28175  swrdccatin2  28176  swrdccatin12lem3c  28177  swrdccatin12lem3  28178  swrdccat3blem  28184  swrdccatin1d  28186  swrdccatin2d  28187  swrdccatin12d  28188  reumodprminv  28193  2cshw1lem1  28214  2cshw1lem2  28215  2cshw2lem2  28219  3cshw  28232  cshweqdif2  28233  cshweqdif2s  28234  cshweqrep  28237  usgra2pthlem1  28263  2wlksot  28287  2spthsot  28288  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  2wlkonot3v  28295  2spthonot3v  28296  el2wlksoton  28298  el2spthsoton  28299  el2wlksotot  28302  usg2spthonot  28308  usg2spthonot0  28309  frgrancvvdeqlem3  28358  usg2spot2nb  28391  usgreg2spot  28393  2spotmdisj  28394  bnj945  29081  bnj1400  29144  bnj18eq1  29235  bnj916  29241  bnj1014  29268  bnj1015  29269  bnj1110  29288  bnj1417  29347  islshp  29714  islsat  29726  lcvfbr  29755  islfl  29795  ellkr  29824  islshpkrN  29855  ldual1dim  29901  isopos  29915  cmtfvalN  29945  cvrfval  30003  isat  30021  islln  30240  islpln  30264  islvol  30307  isline  30473  ispointN  30476  ispsubsp  30479  elpmap  30492  elpmapat  30498  elpadd  30533  paddclN  30576  elpclN  30626  elpcliN  30627  pclfinN  30634  pclcmpatN  30635  ispsubclN  30671  iswatN  30728  islhp  30730  islaut  30817  ispautN  30833  isldil  30844  isltrn  30853  isdilN  30888  istrnN  30891  istendo  31494  dvhb1dimN  31720  erng1lem  31721  erngdvlem4-rN  31733  diaelval  31768  diaeldm  31771  dia1dimid  31798  cdlemm10N  31853  dibopelvalN  31878  dibopelval2  31880  dibelval3  31882  dibelval1st  31884  dibelval2nd  31887  dibeldmN  31893  dibvalrel  31898  dibglbN  31901  dicffval  31909  dicfval  31910  dicopelval  31912  dicelvalN  31913  dicelval3  31915  dicvalrelN  31920  dicelval1sta  31922  diclspsn  31929  dihopelvalbN  31973  dihopelvalcqat  31981  dihopelvalcpre  31983  dihvalrel  32014  dih1  32021  dihmeetlem4preN  32041  dihmeetlem13N  32054  dih1dimatlem  32064  dochnel2  32127  dihjatcclem4  32156  dvh2dim  32180  dvh3dim  32181  dvh4dimN  32182  dochfln0  32212  lpolsetN  32217  islpolN  32218  lcfrvalsnN  32276  lcfrlem21  32298  lcfrlem27  32304  lcfrlem37  32314  lcfr  32320  lcdlss  32354  mapdcv  32395  hdmap1fval  32532  hdmapffval  32564  hdmapfval  32565  hdmapval  32566  hgmapffval  32623  hgmapfval  32624  hdmapellkr  32652  hlhilhillem  32698
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