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

Theorem breq2d 4590
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
breq2d (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Proof of Theorem breq2d
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq2 4582 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475   class class class wbr 4578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579
This theorem is referenced by:  breqtrd  4604  sbcbr1g  4634  pofun  4965  csbfv12  6126  isorel  6454  soisores  6455  soisoi  6456  isocnv  6458  isotr  6464  f1owe  6481  caovordig  6715  caovordg  6717  caovord  6721  f1oweALT  7021  frxp  7152  xporderlem  7153  fnwelem  7157  difsnen  7905  domdifsn  7906  unfilem3  8089  domunfican  8096  marypha1lem  8200  marypha1  8201  inflb  8256  wemapwe  8455  oef1o  8456  r1sdom  8498  sdomsdomcardi  8658  alephordi  8758  pwcdadom  8899  sornom  8960  axdclem  9202  pwcfsdom  9262  elgch  9301  winalim2  9375  rankcf  9456  inatsk  9457  pinq  9606  nqereu  9608  ltaddnq  9653  ltrnq  9658  archnq  9659  addclprlem1  9695  mulclprlem  9698  1idpr  9708  ltaprlem  9723  ltapr  9724  prlem936  9726  ltasr  9778  mulgt0sr  9783  sqgt0sr  9784  map2psrpr  9788  axpre-ltadd  9845  axpre-mulgt0  9846  axpre-sup  9847  ltaddneg  10103  ltsubadd2  10351  lesubadd2  10353  ltaddpos2  10371  posdif  10373  lesub1  10374  ltnegcon1  10381  lenegcon1  10384  addge02  10391  leaddle0  10395  mulge0  10398  msqge0  10401  ltordlem  10405  possumd  10504  sublt0d  10505  prodgt0  10720  prodgt02  10721  prodge02  10723  ltmulgt12  10736  lemulge12  10738  mulge0b  10745  mulle0b  10746  ltdivmul  10750  ledivmul  10751  ltdivmul2  10752  lt2mul2div  10753  ledivmul2  10754  ltrec  10757  ltrec1  10762  ltdiv23  10766  lediv23  10767  nnge1  10896  halfpos  11112  lt2halves  11117  addltmul  11118  avglt2  11121  avgle2  11123  nnrecl  11140  difgtsumgt  11196  zltlem1  11266  gtndiv  11289  nn01to3  11616  rebtwnz  11622  nnledivrp  11775  xrmax1  11842  max1ALT  11853  qbtwnre  11866  xralrple  11872  xltnegi  11883  xmulval  11892  xsubge0  11923  xposdif  11924  xlesubadd  11925  divelunit  12144  eluzgtdifelfzo  12355  fllelt  12418  flflp1  12428  flbi  12437  btwnzge0  12449  2tnp1ge0ge0  12450  dfceil2  12460  ceilval2  12461  2submod  12551  addmodlteq  12565  om2uzlti  12569  monoord  12651  sermono  12653  expval  12682  expnbnd  12813  discr1  12820  discr  12821  facwordi  12896  seqcoll  13060  seqcoll2  13061  hashtpg  13074  swrdccat3blem  13295  cnpart  13777  sqrlem6  13785  sqrmo  13789  resqreu  13790  resqrtcl  13791  resqrtthlem  13792  sqrtneg  13805  sqreulem  13896  sqreu  13897  sqrtthlem  13899  eqsqrtd  13904  limsuple  14006  rlimcld2  14106  rlimrege0  14107  o1compt  14115  climserle  14190  caurcvgr  14201  fsum00  14320  fsumabs  14323  climcndslem2  14370  climcnds  14371  supcvg  14376  georeclim  14391  geoisumr  14397  cvgrat  14403  sin01bnd  14703  cos01bnd  14704  ruclem1  14748  ruclem9  14755  ruclem12  14758  summodnegmod  14799  modmulconst  14800  dvdsaddr  14812  dvdssub  14813  dvdssubr  14814  dvdsfac  14835  dvdsmod  14837  fprodfvdvdsd  14845  oddp1even  14855  ltoddhalfle  14872  opoe  14874  omoe  14875  sumeven  14897  sumodd  14898  divalglem0  14903  divalglem2  14905  divalglem4  14906  divalglem5  14907  divalglem9  14911  divalg  14913  divalg2  14915  divalgmod  14916  divalgmodOLD  14917  ndvdssub  14920  ndvdsadd  14921  bitsfval  14932  bitsval  14933  bits0  14937  bitsp1  14940  bitsfzolem  14943  bitsfzo  14944  bitscmp  14947  bitsinv1lem  14950  bitsshft  14984  gcdcllem1  15008  dvdslegcd  15013  bezoutlem4  15046  dvdssqim  15060  dvdsmulgcd  15061  dvdssq  15067  nn0seqcvgd  15070  lcmfunsnlem2lem2  15139  coprmdvds  15153  coprmdvdsOLD  15154  coprmdvds2  15155  rpmul  15160  cncongr1  15168  divgcdodd  15209  isprm6  15213  prmdvdsexp  15214  prmdvdsexpr  15216  prmfac1  15218  hashdvds  15267  phiprmpw  15268  eulerthlem2  15274  prmdiv  15277  prmdiveq  15278  odzval  15283  odzcllem  15284  odzdvds  15287  pythagtriplem11  15317  pythagtriplem13  15319  pythagtrip  15326  pceulem  15337  pczndvds2  15358  pcdvdsb  15360  pc2dvds  15370  pcz  15372  pcprmpw2  15373  dvdsprmpweq  15375  dvdsprmpweqle  15377  difsqpwdvds  15378  pcaddlem  15379  pcmpt  15383  prmpwdvds  15395  pockthlem  15396  prmreclem2  15408  prmreclem4  15410  4sqlem11  15446  vdwlem9  15480  rami  15506  ramlb  15510  0ram  15511  ramz2  15515  ramub1lem1  15517  prmdvdsprmo  15533  prmgaplem7  15548  prmgaplem8  15549  imasleval  15973  subsubc  16285  pospo  16745  mulgval  17315  oddvdsnn0  17735  odmulg  17745  pgpfi1  17782  pgpfi  17792  slwispgp  17798  pgpssslw  17801  subgslw  17803  sylow2alem2  17805  sylow2blem3  17809  fislw  17812  efgi  17904  efgval2  17909  efgsrel  17919  efgredlemb  17931  lt6abl  18068  telgsums  18162  dprdval  18174  dprd2dlem2  18211  dprd2da  18213  dprd2d2  18215  ablfacrplem  18236  ablfac1a  18240  ablfac1b  18241  ablfac1eulem  18243  ablfac1eu  18244  pgpfac1lem3a  18247  ablfaclem3  18258  dvdsrtr  18424  dvdsrmul1  18425  unitpropd  18469  isabvd  18592  mplval  19198  ressmplbas2  19225  mplbaspropd  19377  zndvds0  19666  znunit  19679  cygth  19687  frlmup1  19904  lmisfree  19948  pmatcoe1fsupp  20273  fvmptnn04if  20421  hmphindis  21358  ordthmeolem  21362  psmettri2  21872  ismet2  21896  xmettri2  21903  imasdsf1olem  21936  imasf1oxmet  21938  comet  22076  stdbdxmet  22078  nmogelb  22278  nmolb  22279  metdsge  22408  metdseq0  22413  iihalf2  22488  bndth  22513  evth  22514  ipcau2  22786  tchcphlem1  22787  tchcphlem2  22788  iscau3  22829  iscmet3  22844  bcthlem1  22874  bcth  22879  minveclem3b  22952  minveclem3  22953  minveclem4  22956  minveclem5  22957  pjthlem1  22961  pjthlem2  22962  pmltpclem1  22969  pmltpc  22971  ivthlem2  22973  ivthlem3  22974  ovolgelb  23000  ovolunlem1  23017  ovoliunlem2  23023  ovolshftlem1  23029  ovolscalem1  23033  ovolicc1  23036  ovolicc2lem3  23039  ioombl1lem4  23081  mbfmulc2lem  23165  mbfposb  23171  mbfaddlem  23178  mbfsup  23182  mbfinf  23183  mbflimsup  23184  i1fposd  23225  itg1ge0a  23229  mbfi1fseqlem4  23236  mbfi1fseqlem6  23238  mbfi1flimlem  23240  mbfi1flim  23241  itg2const2  23259  itg2seq  23260  itg2monolem1  23268  itg2i1fseq  23273  itg2addlem  23276  ibllem  23282  isibl  23283  isibl2  23284  iblitg  23286  dfitg  23287  cbvitg  23293  itgeq2  23295  itgvallem  23302  iblneg  23320  itgneg  23321  itggt0  23359  dvlip  23505  c1lip1  23509  dvfsumle  23533  dvfsumlem2  23539  dvfsumlem4  23541  dvfsum2  23546  mdeglt  23574  degltp1le  23582  deg1suble  23616  ply1divex  23645  plypf1  23717  dgrlb  23741  coemulc  23760  dgrsub  23777  quotval  23796  plydivlem4  23800  quotcan  23813  vieta1lem2  23815  aalioulem2  23837  aaliou3lem9  23854  ulmcn  23902  dvradcnv  23924  sincosq1sgn  23999  sincosq2sgn  24000  sincosq4sgn  24002  logltb  24095  cxpge0  24174  cxple2  24188  logreclem  24245  jensen  24460  emcllem7  24473  lgamgulmlem1  24500  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamgulmlem5  24504  lgambdd  24508  lgamcvglem  24511  wilthlem1  24539  ftalem2  24545  ftalem3  24546  ftalem7  24550  fta  24551  sgmval  24613  mumul  24652  dvdsppwf1o  24657  musum  24662  chtublem  24681  chtub  24682  perfect1  24698  bcmono  24747  bclbnd  24750  bposlem1  24754  bposlem5  24758  lgslem1  24767  lgsval  24771  lgsdilem  24794  lgsne0  24805  lgsqrlem2  24817  lgsqrlem4  24819  gausslemma2dlem1a  24835  lgseisenlem1  24845  lgseisenlem2  24846  lgsquadlem1  24850  lgsquadlem2  24851  lgsquadlem3  24852  lgsquad2lem2  24855  m1lgs  24858  2lgslem1a1  24859  2lgslem1a  24861  2lgsoddprmlem2  24879  2lgsoddprmlem3  24884  2sqlem4  24891  2sqlem8a  24895  2sqblem  24901  dchrisumlema  24922  dchrisumlem2  24924  dchrisumlem3  24925  chpdifbndlem2  24988  pntrsumbnd2  25001  pntpbnd1  25020  pntibndlem3  25026  pntlemi  25038  pntleme  25042  pntlem3  25043  pnt3  25046  ostth2lem2  25068  ostth3  25072  ostth  25073  tgcgrxfr  25159  hlpasch  25394  islmib  25425  lmicom  25426  trgcopyeu  25444  iscgra  25447  iscgra1  25448  iscgrad  25449  isleag  25479  iseqlg  25493  brbtwn2  25531  axlowdim2  25586  axlowdim  25587  axcontlem2  25591  axcontlem3  25592  axcontlem4  25593  axcontlem9  25598  axcontlem10  25599  axcontlem11  25600  axcontlem12  25601  ebtwntg  25608  ausisusgraedg  25679  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  nbhashuvtx1  26236  eupath2lem3  26300  eupath2  26301  konigsberg  26308  frgrareggt1  26437  ex-ind-dvds  26504  nmounbseqi  26810  nmounbseqiALT  26811  isblo3i  26834  blo3i  26835  blocnilem  26837  siilem2  26885  normlem6  27150  normgt0  27162  norm3dif  27185  norm3lemt  27187  pjhthlem1  27428  pjige0  27728  nmcexi  28063  lnconi  28070  lnopcnbd  28073  lnfncnbd  28094  riesz1  28102  cnlnadjlem2  28105  cnlnadjlem8  28111  leopg  28159  leop2  28161  leoppos  28163  leopadd  28169  leopmuli  28170  leopmul2i  28172  pjssge0i  28203  pjdifnormi  28204  pjssposi  28209  pjssdif1i  28212  chcv1  28392  cvexch  28411  atcvatlem  28422  atcvat3i  28433  atdmd  28435  cdj3i  28478  addltmulALT  28483  xrofsup  28717  xrge0addgt0  28816  omndadd  28831  omndmul2  28837  ogrpinvlt  28849  isinftm  28860  isarchi3  28866  archirng  28867  archirngz  28868  archiexdiv  28869  isorng  28924  orngmul  28928  ofldchr  28939  isarchiofld  28942  elrhmunit  28945  rearchi  28967  fzto1st  28978  unitdivcld  29069  esumlub  29243  esumfsup  29253  esumcvg  29269  esum2d  29276  dya2ub  29453  omssubadd  29483  carsgmon  29497  itgeq12dv  29509  oddpwdc  29537  eulerpartlems  29543  prob01  29596  orvcval  29640  ballotlemfc0  29675  ballotlemfcc  29676  ballotleme  29679  ballotlem4  29681  ballotlemimin  29688  ballotlem1c  29690  ballotlemsval  29691  ballotlemieq  29699  ballotlemfrcn0  29712  sgnmulsgp  29733  signsply0  29748  signslema  29759  signsvfpn  29782  erdszelem8  30228  erdsze2lem2  30234  abs2sqle  30622  abs2sqlt  30623  pdivsq  30682  dvdspw  30683  poseq  30788  soseq  30789  sltval  30838  cgrdegen  31075  brofs  31076  segconeu  31082  btwntriv2  31083  transportprops  31105  brifs  31114  ifscgr  31115  brcgr3  31117  cgrxfr  31126  brcolinear2  31129  colineardim1  31132  brfs  31150  idinside  31155  btwnconn1lem11  31168  btwnconn1lem12  31169  btwnconn1lem14  31171  brsegle  31179  seglerflx  31183  seglemin  31184  segleantisym  31186  btwnsegle  31188  outsideofeu  31202  outsidele  31203  fvray  31212  nn0prpwlem  31281  nn0prpw  31282  unblimceq0lem  31461  unbdqndv2  31466  knoppndvlem13  31479  knoppndvlem19  31485  knoppndvlem21  31487  ltflcei  32361  cos2h  32364  tan2h  32365  matunitlindflem2  32370  poimirlem5  32378  poimirlem6  32379  poimirlem7  32380  poimirlem8  32381  poimirlem10  32383  poimirlem11  32384  poimirlem12  32385  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem18  32391  poimirlem19  32392  poimirlem20  32393  poimirlem21  32394  poimirlem22  32395  poimirlem25  32398  poimirlem27  32400  poimirlem28  32401  poimirlem29  32402  poimirlem30  32403  poimirlem31  32404  poimirlem32  32405  poimir  32406  heicant  32408  mblfinlem2  32411  mblfinlem3  32412  mblfinlem4  32413  itg2addnclem  32425  itg2addnclem2  32426  itg2gt0cn  32429  itggt0cn  32446  ftc1anclem5  32453  dvasin  32460  areacirclem1  32464  areacirclem4  32467  areacirclem5  32468  areacirc  32469  seqpo  32507  incsequz2  32509  mettrifi  32517  heibor1lem  32572  rrncmslem  32595  lsatcv0eq  33146  oposlem  33281  oplecon1b  33300  opltcon1b  33304  atlatmstc  33418  cvlexch1  33427  cvlexch2  33428  cvlexchb2  33430  cvlatexchb2  33434  cvlatexch2  33436  cvlatcvr2  33441  cvlsupr2  33442  ishlat1  33451  hlsuprexch  33479  cvrexch  33518  cvrat  33520  atcvr0eq  33524  atcvrj0  33526  atltcvr  33533  cvrat3  33540  cvrat4  33541  cvrat42  33542  3noncolr2  33547  hlatcon2  33550  4noncolr3  33551  3dimlem1  33556  3dimlem2  33557  3dimlem3a  33558  3dimlem3  33559  3dimlem3OLDN  33560  3dimlem4a  33561  3dimlem4  33562  3dimlem4OLDN  33563  3dim1lem5  33564  3dim2  33566  3dim3  33567  ps-1  33575  ps-2  33576  3atlem5  33585  3atlem6  33586  lplni2  33635  lplnnle2at  33639  lplnnleat  33640  lplnnlelln  33641  lplnribN  33649  lplnexllnN  33662  lvoli2  33679  lvolnle3at  33680  lvolnleat  33681  lvolnlelln  33682  lvolnlelpln  33683  4atlem9  33701  4atlem10a  33702  4atlem11a  33705  4atlem11  33707  4atlem12a  33708  dalempnes  33749  dalemqnet  33750  dalem1  33757  dalemswapyzps  33788  dalemrotps  33789  dalem30  33800  dalem35  33805  lineset  33836  islinei  33838  psubspset  33842  psubspi2N  33846  snatpsubN  33848  2llnma1  33885  elpaddn0  33898  elpaddri  33900  elpaddat  33902  elpadd2at  33904  paddcom  33911  paddasslem12  33929  pmapjat1  33951  llnexchb2  33967  lhp2at0nle  34133  lhprelat3N  34138  4atexlemswapqr  34161  4atexlemcnd  34170  lautle  34182  lautcvr  34190  ltrnel  34237  ltrneq2  34246  trlnle  34285  cdlemc3  34292  cdlemd6  34302  cdleme3  34336  cdleme7aa  34341  cdleme7  34348  cdleme11c  34360  cdleme15c  34375  cdleme20yOLD  34402  cdleme20m  34423  cdleme21b  34426  cdleme21c  34427  cdleme21at  34428  cdleme36a  34560  cdleme43bN  34590  cdleme43dN  34592  cdleme46f2g2  34593  cdleme46f2g1  34594  cdlemeg46c  34613  cdlemeg46nlpq  34617  cdlemb3  34706  cdlemg4d  34713  cdlemg6d  34721  cdlemg10c  34739  cdlemg12  34750  cdlemg27b  34796  djhcvat42  35516  elpell1qr2  36248  monotuz  36318  monotoddzzfi  36319  monotoddzz  36320  oddcomabszz  36321  rmxypos  36326  mzpcong  36351  congrep  36352  acongsym  36355  acongneg2  36356  acongtr  36357  acongeq12d  36358  jm2.18  36367  jm2.19lem2  36369  jm2.19lem3  36370  jm2.19lem4  36371  jm2.19  36372  jm2.25  36378  jm2.15nn0  36382  jm2.16nn0  36383  jm2.27  36387  rmydioph  36393  expdiophlem1  36400  expdiophlem2  36401  fnwe2lem2  36433  relexpmulg  36815  relexpxpmin  36822  frege124d  36866  frege72  37043  frege91  37062  inductionexd  37267  leeq2d  37270  imo72b2lem0  37281  imo72b2lem2  37283  imo72b2lem1  37287  imo72b2  37291  dvgrat  37327  hashnzfz  37335  evth2f  37991  evthf  38003  rfcnpre3  38009  brneqtrd  38068  dmrelrnrel  38208  upbdrech2  38257  supxrgelem  38288  supxrge  38289  xrlexaddrp  38303  xralrple2  38305  ltdivgt1  38307  infleinf  38323  xralrple4  38324  xralrple3  38325  ltdiv23neg  38352  fsumlessf  38438  fmul01  38441  fmul01lt1lem1  38445  climinf  38467  climinff  38472  limcrecl  38490  limsupre  38502  limclner  38512  cncficcgt0  38568  stoweidlem3  38690  stoweidlem7  38694  stoweidlem15  38702  stoweidlem16  38703  stoweidlem18  38705  stoweidlem26  38713  stoweidlem27  38714  stoweidlem28  38715  stoweidlem31  38718  stoweidlem34  38721  stoweidlem36  38723  stoweidlem37  38724  stoweidlem41  38728  stoweidlem44  38731  stoweidlem45  38732  stoweidlem46  38733  stoweidlem48  38735  stoweidlem51  38738  stoweidlem55  38742  stoweidlem59  38746  stoweidlem60  38747  stoweidlem62  38749  fourierdlem42  38836  fourierdlem50  38843  fourierdlem54  38847  fourierdlem68  38861  fourierdlem79  38872  fourierdlem96  38889  fourierdlem97  38890  fourierdlem98  38891  fourierdlem99  38892  fourierdlem105  38898  fourierdlem108  38901  fourierdlem110  38903  fourierdlem111  38904  etransclem24  38945  etransclem25  38946  etransclem35  38956  etransclem37  38958  etransclem41  38962  etransclem44  38965  sge0gerp  39082  sge0pnffigt  39083  sge0gerpmpt  39089  omessle  39182  ovncvrrp  39248  ovnsubaddlem1  39254  ovnsubadd  39256  hoidmv1lelem2  39276  hoidmvlelem3  39281  hoidmvle  39284  ovncvr2  39295  hoidifhspval2  39299  hoidifhspval3  39303  hspmbllem2  39311  hspmbl  39313  pimgtpnf2  39388  pimgtmnf2  39395  pimdecfgtioc  39396  pimdecfgtioo  39398  pimincfltioo  39399  pimgtmnf  39403  incsmf  39423  issmfgt  39437  decsmf  39447  smfpreimagtf  39448  issmfge  39450  smflimlem4  39454  smflim  39457  smfpimgtxr  39460  smfpimgtmpt  39461  smfpimgtxrmpt  39464  smonoord  39739  iccpartiltu  39755  iccpartlt  39757  iccpartgtl  39759  iccpartgt  39760  iccpartgel  39762  iccpartrn  39763  iccpartiun  39767  icceuelpartlem  39768  iccpartdisj  39770  iccpartnel  39771  goldbachthlem2  39791  fmtnoprmfac1lem  39809  fmtnoprmfac1  39810  fmtnofac1  39815  2pwp1prm  39836  flsqrt  39841  lighneallem1  39855  lighneallem3  39857  lighneallem4  39860  bits0ALTV  39923  sgoldbaltlem1  39996  bgoldbtbndlem2  40017  bgoldbtbndlem3  40018  bgoldbtbnd  40020  ltsubsubaddltsub  40164  subsubelfzo0  40176  umgrislfupgrlem  40339  lfgredgge2  40341  lfgrnloop  40342  lfuhgr1v0e  40472  1hevtxdg1  40713  1hegrlfgr  40714  ewlksfval  40795  isewlk  40796  ewlkinedg  40798  lfgrwlkprop  40888  crctcshlem4  41015  umgrwwlks2on  41153  elwwlks2  41162  clwlkclwwlklem2a4  41198  clwlkclwwlklem2a  41199  eupth2lem3lem3  41390  eupth2lem3lem4  41391  eupth2lem3lem6  41393  eupth2lem3lem7  41394  eupth2lems  41398  eupth2  41399  eucrct2eupth  41405  konigsberglem4  41417  av-frgrareggt1  41539  nn0le2is012  41930  lcoop  41986  islininds  42021  ldepsnlinc  42083  ltsubaddb  42090  ltsubsubb  42091  ltsubadd2b  42092  logle1b  42117  loglt1b  42118  bigoval  42133  elbigo2r  42137  logbge0b  42147  logblt1b  42148  fldivexpfllog2  42149  nnlog2ge0lt1  42150  fllog2  42152  nnpw2pmod  42167  dignn0ldlem  42186  dig2nn1st  42189
  Copyright terms: Public domain W3C validator