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

Theorem breq2d 4595
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 4587 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475   class class class wbr 4583
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 4584
This theorem is referenced by:  breqtrd  4609  sbcbr1g  4639  pofun  4975  csbfv12  6141  isorel  6476  soisores  6477  soisoi  6478  isocnv  6480  isotr  6486  f1owe  6503  caovordig  6737  caovordg  6739  caovord  6743  f1oweALT  7043  frxp  7174  xporderlem  7175  fnwelem  7179  difsnen  7927  domdifsn  7928  unfilem3  8111  domunfican  8118  marypha1lem  8222  marypha1  8223  inflb  8278  wemapwe  8477  oef1o  8478  r1sdom  8520  sdomsdomcardi  8680  alephordi  8780  pwcdadom  8921  sornom  8982  axdclem  9224  pwcfsdom  9284  elgch  9323  winalim2  9397  rankcf  9478  inatsk  9479  pinq  9628  nqereu  9630  ltaddnq  9675  ltrnq  9680  archnq  9681  addclprlem1  9717  mulclprlem  9720  1idpr  9730  ltaprlem  9745  ltapr  9746  prlem936  9748  ltasr  9800  mulgt0sr  9805  sqgt0sr  9806  map2psrpr  9810  axpre-ltadd  9867  axpre-mulgt0  9868  axpre-sup  9869  ltaddneg  10130  ltsubadd2  10378  lesubadd2  10380  ltaddpos2  10398  posdif  10400  lesub1  10401  ltnegcon1  10408  lenegcon1  10411  addge02  10418  leaddle0  10422  mulge0  10425  msqge0  10428  ltordlem  10432  possumd  10531  sublt0d  10532  prodgt0  10747  prodgt02  10748  prodge02  10750  ltmulgt12  10763  lemulge12  10765  mulge0b  10772  mulle0b  10773  ltdivmul  10777  ledivmul  10778  ltdivmul2  10779  lt2mul2div  10780  ledivmul2  10781  ltrec  10784  ltrec1  10789  ltdiv23  10793  lediv23  10794  nnge1  10923  halfpos  11139  lt2halves  11144  addltmul  11145  avglt2  11148  avgle2  11150  nnrecl  11167  difgtsumgt  11223  zltlem1  11307  gtndiv  11330  nn01to3  11657  rebtwnz  11663  nnledivrp  11816  xrmax1  11880  max1ALT  11891  qbtwnre  11904  xralrple  11910  xltnegi  11921  xmulval  11930  xsubge0  11963  xposdif  11964  xlesubadd  11965  divelunit  12185  eluzgtdifelfzo  12397  fllelt  12460  flflp1  12470  flbi  12479  btwnzge0  12491  2tnp1ge0ge0  12492  dfceil2  12502  ceilval2  12503  2submod  12593  addmodlteq  12607  om2uzlti  12611  monoord  12693  sermono  12695  expval  12724  expnbnd  12855  discr1  12862  discr  12863  facwordi  12938  seqcoll  13105  seqcoll2  13106  hashtpg  13121  swrdccat3blem  13346  cnpart  13828  sqrlem6  13836  sqrmo  13840  resqreu  13841  resqrtcl  13842  resqrtthlem  13843  sqrtneg  13856  sqreulem  13947  sqreu  13948  sqrtthlem  13950  eqsqrtd  13955  limsuple  14057  rlimcld2  14157  rlimrege0  14158  o1compt  14166  climserle  14241  caurcvgr  14252  fsum00  14371  fsumabs  14374  climcndslem2  14421  climcnds  14422  supcvg  14427  georeclim  14442  geoisumr  14448  cvgrat  14454  sin01bnd  14754  cos01bnd  14755  ruclem1  14799  ruclem9  14806  ruclem12  14809  summodnegmod  14850  modmulconst  14851  dvdsaddr  14863  dvdssub  14864  dvdssubr  14865  dvdsfac  14886  dvdsmod  14888  fprodfvdvdsd  14896  oddp1even  14906  ltoddhalfle  14923  opoe  14925  omoe  14926  sumeven  14948  sumodd  14949  divalglem0  14954  divalglem2  14956  divalglem4  14957  divalglem5  14958  divalglem9  14962  divalg  14964  divalg2  14966  divalgmod  14967  divalgmodOLD  14968  ndvdssub  14971  ndvdsadd  14972  bitsfval  14983  bitsval  14984  bits0  14988  bitsp1  14991  bitsfzolem  14994  bitsfzo  14995  bitscmp  14998  bitsinv1lem  15001  bitsshft  15035  gcdcllem1  15059  dvdslegcd  15064  bezoutlem4  15097  dvdssqim  15111  dvdsmulgcd  15112  dvdssq  15118  nn0seqcvgd  15121  lcmfunsnlem2lem2  15190  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  rpmul  15211  cncongr1  15219  divgcdodd  15260  isprm6  15264  prmdvdsexp  15265  prmdvdsexpr  15267  prmfac1  15269  hashdvds  15318  phiprmpw  15319  eulerthlem2  15325  prmdiv  15328  prmdiveq  15329  odzval  15334  odzcllem  15335  odzdvds  15338  pythagtriplem11  15368  pythagtriplem13  15370  pythagtrip  15377  pceulem  15388  pczndvds2  15409  pcdvdsb  15411  pc2dvds  15421  pcz  15423  pcprmpw2  15424  dvdsprmpweq  15426  dvdsprmpweqle  15428  difsqpwdvds  15429  pcaddlem  15430  pcmpt  15434  prmpwdvds  15446  pockthlem  15447  prmreclem2  15459  prmreclem4  15461  4sqlem11  15497  vdwlem9  15531  rami  15557  ramlb  15561  0ram  15562  ramz2  15566  ramub1lem1  15568  prmdvdsprmo  15584  prmgaplem7  15599  prmgaplem8  15600  imasleval  16024  subsubc  16336  pospo  16796  mulgval  17366  oddvdsnn0  17786  odmulg  17796  pgpfi1  17833  pgpfi  17843  slwispgp  17849  pgpssslw  17852  subgslw  17854  sylow2alem2  17856  sylow2blem3  17860  fislw  17863  efgi  17955  efgval2  17960  efgsrel  17970  efgredlemb  17982  lt6abl  18119  telgsums  18213  dprdval  18225  dprd2dlem2  18262  dprd2da  18264  dprd2d2  18266  ablfacrplem  18287  ablfac1a  18291  ablfac1b  18292  ablfac1eulem  18294  ablfac1eu  18295  pgpfac1lem3a  18298  ablfaclem3  18309  dvdsrtr  18475  dvdsrmul1  18476  unitpropd  18520  isabvd  18643  mplval  19249  ressmplbas2  19276  mplbaspropd  19428  zndvds0  19718  znunit  19731  cygth  19739  frlmup1  19956  lmisfree  20000  pmatcoe1fsupp  20325  fvmptnn04if  20473  hmphindis  21410  ordthmeolem  21414  psmettri2  21924  ismet2  21948  xmettri2  21955  imasdsf1olem  21988  imasf1oxmet  21990  comet  22128  stdbdxmet  22130  nmogelb  22330  nmolb  22331  metdsge  22460  metdseq0  22465  iihalf2  22540  bndth  22565  evth  22566  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  iscau3  22884  iscmet3  22899  bcthlem1  22929  bcth  22934  minveclem3b  23007  minveclem3  23008  minveclem4  23011  minveclem5  23012  pjthlem1  23016  pjthlem2  23017  pmltpclem1  23024  pmltpc  23026  ivthlem2  23028  ivthlem3  23029  ovolgelb  23055  ovolunlem1  23072  ovoliunlem2  23078  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem3  23094  ioombl1lem4  23136  mbfmulc2lem  23220  mbfposb  23226  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  mbflimsup  23239  i1fposd  23280  itg1ge0a  23284  mbfi1fseqlem4  23291  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfi1flim  23296  itg2const2  23314  itg2seq  23315  itg2monolem1  23323  itg2i1fseq  23328  itg2addlem  23331  ibllem  23337  isibl  23338  isibl2  23339  iblitg  23341  dfitg  23342  cbvitg  23348  itgeq2  23350  itgvallem  23357  iblneg  23375  itgneg  23376  itggt0  23414  dvlip  23560  c1lip1  23564  dvfsumle  23588  dvfsumlem2  23594  dvfsumlem4  23596  dvfsum2  23601  mdeglt  23629  degltp1le  23637  deg1suble  23671  ply1divex  23700  plypf1  23772  dgrlb  23796  coemulc  23815  dgrsub  23832  quotval  23851  plydivlem4  23855  quotcan  23868  vieta1lem2  23870  aalioulem2  23892  aaliou3lem9  23909  ulmcn  23957  dvradcnv  23979  sincosq1sgn  24054  sincosq2sgn  24055  sincosq4sgn  24057  logltb  24150  cxpge0  24229  cxple2  24243  logreclem  24300  jensen  24515  emcllem7  24528  lgamgulmlem1  24555  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  lgamcvglem  24566  wilthlem1  24594  ftalem2  24600  ftalem3  24601  ftalem7  24605  fta  24606  sgmval  24668  mumul  24707  dvdsppwf1o  24712  musum  24717  chtublem  24736  chtub  24737  perfect1  24753  bcmono  24802  bclbnd  24805  bposlem1  24809  bposlem5  24813  lgslem1  24822  lgsval  24826  lgsdilem  24849  lgsne0  24860  lgsqrlem2  24872  lgsqrlem4  24874  gausslemma2dlem1a  24890  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem2  24910  m1lgs  24913  2lgslem1a1  24914  2lgslem1a  24916  2lgsoddprmlem2  24934  2lgsoddprmlem3  24939  2sqlem4  24946  2sqlem8a  24950  2sqblem  24956  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  chpdifbndlem2  25043  pntrsumbnd2  25056  pntpbnd1  25075  pntibndlem3  25081  pntlemi  25093  pntleme  25097  pntlem3  25098  pnt3  25101  ostth2lem2  25123  ostth3  25127  ostth  25128  tgcgrxfr  25213  hlpasch  25448  islmib  25479  lmicom  25480  trgcopyeu  25498  iscgra  25501  iscgra1  25502  iscgrad  25503  isleag  25533  iseqlg  25547  brbtwn2  25585  axlowdim2  25640  axlowdim  25641  axcontlem2  25645  axcontlem3  25646  axcontlem4  25647  axcontlem9  25652  axcontlem10  25653  axcontlem11  25654  axcontlem12  25655  ebtwntg  25662  umgrislfupgrlem  25788  lfgredgge2  25790  lfgrnloop  25791  ausisusgraedg  25885  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  nbhashuvtx1  26442  eupath2lem3  26506  eupath2  26507  konigsberg  26514  frgrareggt1  26643  ex-ind-dvds  26710  nmounbseqi  27016  nmounbseqiALT  27017  isblo3i  27040  blo3i  27041  blocnilem  27043  siilem2  27091  normlem6  27356  normgt0  27368  norm3dif  27391  norm3lemt  27393  pjhthlem1  27634  pjige0  27934  nmcexi  28269  lnconi  28276  lnopcnbd  28279  lnfncnbd  28300  riesz1  28308  cnlnadjlem2  28311  cnlnadjlem8  28317  leopg  28365  leop2  28367  leoppos  28369  leopadd  28375  leopmuli  28376  leopmul2i  28378  pjssge0i  28409  pjdifnormi  28410  pjssposi  28415  pjssdif1i  28418  chcv1  28598  cvexch  28617  atcvatlem  28628  atcvat3i  28639  atdmd  28641  cdj3i  28684  addltmulALT  28689  xrofsup  28923  xrge0addgt0  29022  omndadd  29037  omndmul2  29043  ogrpinvlt  29055  isinftm  29066  isarchi3  29072  archirng  29073  archirngz  29074  archiexdiv  29075  isorng  29130  orngmul  29134  ofldchr  29145  isarchiofld  29148  elrhmunit  29151  rearchi  29173  fzto1st  29184  unitdivcld  29275  esumlub  29449  esumfsup  29459  esumcvg  29475  esum2d  29482  dya2ub  29659  omssubadd  29689  carsgmon  29703  itgeq12dv  29715  oddpwdc  29743  eulerpartlems  29749  prob01  29802  orvcval  29846  ballotlemfc0  29881  ballotlemfcc  29882  ballotleme  29885  ballotlem4  29887  ballotlemimin  29894  ballotlem1c  29896  ballotlemsval  29897  ballotlemieq  29905  ballotlemfrcn0  29918  sgnmulsgp  29939  signsply0  29954  signslema  29965  signsvfpn  29988  erdszelem8  30434  erdsze2lem2  30440  abs2sqle  30828  abs2sqlt  30829  pdivsq  30888  dvdspw  30889  poseq  30994  soseq  30995  sltval  31044  cgrdegen  31281  brofs  31282  segconeu  31288  btwntriv2  31289  transportprops  31311  brifs  31320  ifscgr  31321  brcgr3  31323  cgrxfr  31332  brcolinear2  31335  colineardim1  31338  brfs  31356  idinside  31361  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn1lem14  31377  brsegle  31385  seglerflx  31389  seglemin  31390  segleantisym  31392  btwnsegle  31394  outsideofeu  31408  outsidele  31409  fvray  31418  nn0prpwlem  31487  nn0prpw  31488  unblimceq0lem  31667  unbdqndv2  31672  knoppndvlem13  31685  knoppndvlem19  31691  knoppndvlem21  31693  ltflcei  32567  cos2h  32570  tan2h  32571  matunitlindflem2  32576  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnclem2  32632  itg2gt0cn  32635  itggt0cn  32652  ftc1anclem5  32659  dvasin  32666  areacirclem1  32670  areacirclem4  32673  areacirclem5  32674  areacirc  32675  seqpo  32713  incsequz2  32715  mettrifi  32723  heibor1lem  32778  rrncmslem  32801  lsatcv0eq  33352  oposlem  33487  oplecon1b  33506  opltcon1b  33510  atlatmstc  33624  cvlexch1  33633  cvlexch2  33634  cvlexchb2  33636  cvlatexchb2  33640  cvlatexch2  33642  cvlatcvr2  33647  cvlsupr2  33648  ishlat1  33657  hlsuprexch  33685  cvrexch  33724  cvrat  33726  atcvr0eq  33730  atcvrj0  33732  atltcvr  33739  cvrat3  33746  cvrat4  33747  cvrat42  33748  3noncolr2  33753  hlatcon2  33756  4noncolr3  33757  3dimlem1  33762  3dimlem2  33763  3dimlem3a  33764  3dimlem3  33765  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  3dim1lem5  33770  3dim2  33772  3dim3  33773  ps-1  33781  ps-2  33782  3atlem5  33791  3atlem6  33792  lplni2  33841  lplnnle2at  33845  lplnnleat  33846  lplnnlelln  33847  lplnribN  33855  lplnexllnN  33868  lvoli2  33885  lvolnle3at  33886  lvolnleat  33887  lvolnlelln  33888  lvolnlelpln  33889  4atlem9  33907  4atlem10a  33908  4atlem11a  33911  4atlem11  33913  4atlem12a  33914  dalempnes  33955  dalemqnet  33956  dalem1  33963  dalemswapyzps  33994  dalemrotps  33995  dalem30  34006  dalem35  34011  lineset  34042  islinei  34044  psubspset  34048  psubspi2N  34052  snatpsubN  34054  2llnma1  34091  elpaddn0  34104  elpaddri  34106  elpaddat  34108  elpadd2at  34110  paddcom  34117  paddasslem12  34135  pmapjat1  34157  llnexchb2  34173  lhp2at0nle  34339  lhprelat3N  34344  4atexlemswapqr  34367  4atexlemcnd  34376  lautle  34388  lautcvr  34396  ltrnel  34443  ltrneq2  34452  trlnle  34491  cdlemc3  34498  cdlemd6  34508  cdleme3  34542  cdleme7aa  34547  cdleme7  34554  cdleme11c  34566  cdleme15c  34581  cdleme20yOLD  34608  cdleme20m  34629  cdleme21b  34632  cdleme21c  34633  cdleme21at  34634  cdleme36a  34766  cdleme43bN  34796  cdleme43dN  34798  cdleme46f2g2  34799  cdleme46f2g1  34800  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdlemb3  34912  cdlemg4d  34919  cdlemg6d  34927  cdlemg10c  34945  cdlemg12  34956  cdlemg27b  35002  djhcvat42  35722  elpell1qr2  36454  monotuz  36524  monotoddzzfi  36525  monotoddzz  36526  oddcomabszz  36527  rmxypos  36532  mzpcong  36557  congrep  36558  acongsym  36561  acongneg2  36562  acongtr  36563  acongeq12d  36564  jm2.18  36573  jm2.19lem2  36575  jm2.19lem3  36576  jm2.19lem4  36577  jm2.19  36578  jm2.25  36584  jm2.15nn0  36588  jm2.16nn0  36589  jm2.27  36593  rmydioph  36599  expdiophlem1  36606  expdiophlem2  36607  fnwe2lem2  36639  relexpmulg  37021  relexpxpmin  37028  frege124d  37072  frege72  37249  frege91  37268  inductionexd  37473  leeq2d  37476  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  dvgrat  37533  hashnzfz  37541  evth2f  38197  evthf  38209  rfcnpre3  38215  brneqtrd  38274  dmrelrnrel  38414  upbdrech2  38463  supxrgelem  38494  supxrge  38495  xrlexaddrp  38509  xralrple2  38511  ltdivgt1  38513  infleinf  38529  xralrple4  38530  xralrple3  38531  ltdiv23neg  38558  fsumlessf  38644  fmul01  38647  fmul01lt1lem1  38651  climinf  38673  climinff  38678  limcrecl  38696  limsupre  38708  limclner  38718  cncficcgt0  38774  stoweidlem3  38896  stoweidlem7  38900  stoweidlem15  38908  stoweidlem16  38909  stoweidlem18  38911  stoweidlem26  38919  stoweidlem27  38920  stoweidlem28  38921  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem37  38930  stoweidlem41  38934  stoweidlem44  38937  stoweidlem45  38938  stoweidlem46  38939  stoweidlem48  38941  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  fourierdlem42  39042  fourierdlem50  39049  fourierdlem54  39053  fourierdlem68  39067  fourierdlem79  39078  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem105  39104  fourierdlem108  39107  fourierdlem110  39109  fourierdlem111  39110  etransclem24  39151  etransclem25  39152  etransclem35  39162  etransclem37  39164  etransclem41  39168  etransclem44  39171  sge0gerp  39288  sge0pnffigt  39289  sge0gerpmpt  39295  omessle  39388  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  hoidmv1lelem2  39482  hoidmvlelem3  39487  hoidmvle  39490  ovncvr2  39501  hoidifhspval2  39505  hoidifhspval3  39509  hspmbllem2  39517  hspmbl  39519  pimgtpnf2  39594  pimgtmnf2  39601  pimdecfgtioc  39602  pimdecfgtioo  39604  pimincfltioo  39605  pimgtmnf  39609  incsmf  39629  issmfgt  39643  decsmf  39653  smfpreimagtf  39654  issmfge  39656  smflimlem4  39660  smflim  39663  smfpimgtxr  39666  smfpimgtmpt  39667  smfpimgtxrmpt  39670  smonoord  39944  iccpartiltu  39960  iccpartlt  39962  iccpartgtl  39964  iccpartgt  39965  iccpartgel  39967  iccpartrn  39968  iccpartiun  39972  icceuelpartlem  39973  iccpartdisj  39975  iccpartnel  39976  goldbachthlem2  39996  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnofac1  40020  2pwp1prm  40041  flsqrt  40046  lighneallem1  40060  lighneallem3  40062  lighneallem4  40065  bits0ALTV  40128  sgoldbaltlem1  40201  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  ltsubsubaddltsub  40347  subsubelfzo0  40359  lfuhgr1v0e  40480  1hevtxdg1  40721  1hegrlfgr  40722  ewlksfval  40803  isewlk  40804  ewlkinedg  40806  lfgrwlkprop  40896  crctcshlem4  41023  umgrwwlks2on  41161  elwwlks2  41170  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  eupth2lem3lem3  41398  eupth2lem3lem4  41399  eupth2lem3lem6  41401  eupth2lem3lem7  41402  eupth2lems  41406  eupth2  41407  eucrct2eupth  41413  konigsberglem4  41425  av-frgrareggt1  41547  nn0le2is012  41938  lcoop  41994  islininds  42029  ldepsnlinc  42091  ltsubaddb  42098  ltsubsubb  42099  ltsubadd2b  42100  logle1b  42125  loglt1b  42126  bigoval  42141  elbigo2r  42145  logbge0b  42155  logblt1b  42156  fldivexpfllog2  42157  nnlog2ge0lt1  42158  fllog2  42160  nnpw2pmod  42175  dignn0ldlem  42194  dig2nn1st  42197
  Copyright terms: Public domain W3C validator