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

Theorem breq1 4445
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 4208 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21eleq1d 2531 . 2  |-  ( A  =  B  ->  ( <. A ,  C >.  e.  R  <->  <. B ,  C >.  e.  R ) )
3 df-br 4443 . 2  |-  ( A R C  <->  <. A ,  C >.  e.  R )
4 df-br 4443 . 2  |-  ( B R C  <->  <. B ,  C >.  e.  R )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374    e. wcel 1762   <.cop 4028   class class class wbr 4442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443
This theorem is referenced by:  breq12  4447  breq1i  4449  breq1d  4452  nbrne2  4460  brab1  4487  pocl  4802  swopolem  4804  swopo  4805  solin  4818  sotrieq  4822  sotr2  4824  isso2i  4827  somo  4829  frirr  4851  fr2nr  4852  wereu2  4871  vtoclr  5038  frsn  5064  brcog  5162  brcogw  5164  opelcnvg  5175  dfdmf  5189  eldmg  5191  dfrnf  5234  dfres2  5319  imasng  5352  asymref2  5377  sotri2  5389  somin1  5396  coi1  5516  dffun6f  5595  funmo  5597  fun11  5646  fveq2  5859  eliman0  5888  nfunsn  5890  dffv2  5933  fvopab5  5966  dff3  6027  f1ompt  6036  fmptco  6047  dff13  6147  foeqcnvco  6184  isorel  6203  soisores  6204  soisoi  6205  isocnv  6207  isotr  6213  isomin  6214  isoini  6215  isopolem  6222  isosolem  6224  f1oiso  6228  f1oiso2  6229  weniso  6231  caovordig  6457  caovordg  6459  caovord3d  6462  caovord  6463  caovord3  6465  caofrss  6550  caoftrn  6552  fr3nr  6588  dfwe2  6590  f1oweALT  6760  frxp  6885  poxp  6887  fnse  6892  brtpos2  6953  rntpos  6960  tpostpos  6967  ertr  7318  ecopovsym  7405  ecopovtrn  7406  isfi  7531  en0  7570  en1  7574  endisj  7596  xpcomco  7599  sbth  7629  2pwne  7665  disjenex  7667  ssenen  7683  nneneq  7692  php  7693  sdom1  7711  isinf  7725  fineqvlem  7726  pssnn  7730  enp1i  7746  findcard  7750  findcard2  7751  findcard3  7754  frfi  7756  fiint  7788  mapfienlem1  7855  mapfienlem2  7856  mapfienlem3  7857  mapfien  7858  marypha1lem  7884  supmo  7903  eqsup  7907  supub  7910  suplub  7911  supmaxlem  7915  suppr  7920  supisolem  7922  supisoex  7923  ordtypecbv  7933  ordtypelem3  7936  ordtypelem6  7939  ordtypelem7  7940  ordtypelem9  7942  ordtypelem10  7943  hartogslem1  7958  hartogs  7960  wemaplem1  7962  wemaplem2  7963  wemapso2lem  7969  card2on  7971  card2inf  7972  elharval  7980  brwdom2  7990  wdomtr  7992  cantnfs  8076  cantnfp1lem2  8089  oemapso  8092  cantnflem1  8099  cantnfp1lem2OLD  8115  cantnflem1OLD  8122  wemapwe  8130  wemapweOLD  8131  r111  8184  kardex  8303  karden  8304  isnumi  8318  tskwe  8322  cardid2  8325  cardonle  8329  cardne  8337  iscard2  8348  infxpenlem  8382  fodomfi2  8432  wdomfil  8433  wdomnumr  8436  alephsuc2  8452  infenaleph  8463  iunfictbso  8486  infpss  8588  cff1  8629  cfslb2n  8639  sornom  8648  fin4i  8669  isfin6  8671  isfin7  8672  isfin1-3  8757  fin1a2lem9  8779  fin1a2lem11  8781  hsmexlem4  8800  axcc2lem  8807  axcc4dom  8812  domtriomlem  8813  numthcor  8865  zorn2lem2  8868  zorn2lem3  8869  zorn2lem7  8873  zorn2g  8874  axdclem  8890  axdc  8892  brdom7disj  8900  brdom6disj  8901  uniimadom  8910  ondomon  8929  alephval2  8938  alephreg  8948  pwcfsdom  8949  elgch  8991  gchi  8993  fpwwe2lem12  9010  fpwwe2lem13  9011  pwfseqlem4  9031  winainflem  9062  winalim2  9065  tsken  9123  0tsk  9124  inar1  9144  tskord  9149  tskuni  9152  grudomon  9186  pinq  9296  nqereu  9298  enqeq  9303  ltbtwnnq  9347  ltrnq  9348  prcdnq  9362  prnmax  9364  genpnmax  9376  nqpr  9383  1idpr  9398  reclem2pr  9417  reclem3pr  9418  reclem4pr  9419  recexpr  9420  supexpr  9423  ltsosr  9462  1ne0sr  9464  ltasr  9468  supsrlem  9479  axpre-lttri  9533  axpre-lttrn  9534  axpre-ltadd  9535  axpre-sup  9537  lelttr  9666  dedekind  9734  dedekindle  9735  ltordlem  10069  lt0ne0d  10109  fimaxre3  10483  lbreu  10484  lble  10486  sup2  10490  infm3  10493  suprleub  10498  supmul1  10499  supmullem1  10500  supmul  10502  nnsub  10565  nominpos  10766  nnunb  10782  arch  10783  nn0sub  10837  nn0n0n1ge2b  10851  zextle  10925  peano5uzti  10941  fzind  10950  btwnz  10954  uzval  11075  uzwo  11135  uzwoOLD  11136  nnwof  11139  uzinfmi  11152  ublbneg  11157  lbzbi  11161  zsupss  11162  uzsupss  11165  uzwo3  11168  zmax  11170  rebtwnz  11172  rpnnen1lem3  11201  xrltnsym  11334  xrlttri  11336  xrlttr  11337  xrlelttr  11350  nltpnft  11358  xrmaxlt  11373  xrmaxle  11375  qbtwnre  11389  qbtwnxr  11390  xltnegi  11406  xsubge0  11444  xlesubadd  11446  xmullem2  11448  xlemul1a  11471  xrinfmexpnf  11488  xrsupsslem  11489  xrinfmsslem  11490  xrub  11494  supxrunb1  11502  supxrunb2  11503  ixxval  11528  elixx1  11529  elioo2  11561  iccid  11565  icc0  11568  fzval  11665  elfz1  11668  elfznelfzo  11874  elfznelfzob  11875  flval  11890  fllelt  11893  flval2  11908  flval3  11909  flbi  11910  dfceil2  11926  ceilval2  11927  fleqceilz  11939  modid2  11981  fsequb2  12044  ssnn0fi  12052  seqf1olem2  12105  sqlecan  12231  faclbnd4lem1  12328  pr2pwpr  12475  swrdccatid  12674  sgnval  12873  sqrlem6  13033  01sqrex  13035  abslt  13098  absle  13099  rexanre  13130  rexico  13137  limsupgle  13251  limsupgre  13255  limsupbnd2  13257  rlim2lt  13271  rlim3  13272  ello12r  13291  ello1d  13297  elo12r  13302  rlimconst  13318  climshft  13350  rlimcn2  13364  o1rlimmul  13392  lo1le  13425  climsup  13443  caucvgrlem  13446  isumless  13611  divrcnv  13618  cvgrat  13646  rpnnen2lem10  13809  ruclem1  13816  ruclem2  13817  ruclem11  13825  ruclem12  13826  sqr2irr  13834  absdvdsb  13854  dvdsle  13881  dvdseq  13883  dvdsext  13887  divalglem8  13908  divalglem9  13909  divalglem10  13910  divalgmod  13914  ndvdssub  13915  sadcaddlem  13957  gcdcllem1  13999  gcdcllem2  14000  gcdcllem3  14001  gcdeq  14040  dvdssq  14048  nn0seqcvgd  14049  algcvgblem  14056  1nprm  14072  1idssfct  14073  isprm2lem  14074  isprm2  14075  dvdsprime  14080  nprm  14081  3prm  14084  dvdsprm  14090  coprm  14091  exprmfct  14101  isprm5  14103  maxprmfct  14104  eulerthlem2  14162  odzval  14168  pythagtriplem4  14193  pc2dvds  14252  pcprmpw2  14255  pcprmpw  14256  prmpwdvds  14272  pockthg  14274  unbenlem  14276  prmreclem4  14287  prmreclem5  14288  prmreclem6  14289  1arith  14295  vdwlem6  14354  vdwlem11  14359  vdwlem13  14361  ramtlecl  14368  ramub  14381  rami  14383  ramubcl  14386  0ram  14388  ram0  14390  prmlem0  14440  prmlem1a  14441  imasaddfnlem  14774  imasvscafn  14783  imasleval  14787  prslem  15409  drsdir  15413  drsdirfi  15416  isdrs2  15417  posi  15428  posasymb  15430  pltval3  15445  plelttr  15450  pospo  15451  lubprop  15464  luble  15465  lublecllem  15466  glbprop  15477  joinval2lem  15486  joinlem  15489  meetlem  15503  meetle  15506  latnlej  15546  isglbd  15595  lubub  15597  lubun  15601  clatleglb  15604  pospropd  15612  poslubmo  15624  posglbmo  15625  poslubd  15626  tsrlin  15697  letsr  15705  dirge  15715  pmtrval  16267  pmtrrn  16273  pmtrfrn  16274  pmtrrn2  16276  pmtrsn  16335  mndodcongi  16358  odeq  16365  odmulgeq  16370  gexnnod  16399  sylow1lem1  16409  pgpssslw  16425  sylow2a  16430  efgredeu  16561  efgred2  16562  gexex  16647  frgpnabllem2  16664  cyggenod  16673  dprdval  16820  dprdvalOLD  16822  dprdw  16829  ablfacrplem  16901  ablfac1c  16907  ablfac1eu  16909  ablfaclem3  16923  abvtrivd  17267  psrbagconcl  17791  psrbagconf1o  17792  gsumbagdiaglem  17793  psrmulcllem  17806  psrlidm  17822  psrlidmOLD  17823  psrridm  17824  psrridmOLD  17825  psrass1  17826  psrcom  17830  mplelbas  17853  mplmonmul  17892  ltbwe  17903  coe1fsupp  18020  coe1ae0  18023  coe1mul2  18076  coe1tmmul  18084  zringlpir  18274  zlpir  18279  prmirredlem  18285  prmirredlemOLD  18288  znleval  18355  frlmelbas  18550  ellspd  18598  islindf4  18635  pmatcoe1fsupp  18964  chfacffsupp  19119  chfacfscmulfsupp  19122  chfacfscmulgsum  19123  chfacfpmmulfsupp  19126  chfacfpmmulgsum  19127  ordtbas2  19453  ordtopn2  19457  ordtrest2lem  19465  pnfnei  19482  ordtt1  19641  ordthauslem  19645  2ndci  19710  2ndcsb  19711  2ndcredom  19712  2ndc1stc  19713  1stcrest  19715  2ndcctbss  19717  2ndcdisj  19718  2ndcsep  19721  lly1stc  19758  tx1stc  19881  ordthmeolem  20032  ufildom1  20157  xmetrtri2  20589  prdsxmetlem  20601  ssblex  20661  prdsbl  20724  comet  20746  stdbdxmet  20748  stdbdmopn  20751  met1stc  20754  dscmet  20823  metdstri  21085  metdscn  21090  xrhmeo  21176  bndth  21188  evth  21189  lebnumlem3  21193  pcovalg  21242  pco1  21245  pcocn  21247  pcopt  21252  pcopt2  21253  pcoass  21254  nmoleub3  21332  bcthlem5  21497  rrxfsupp  21559  minveclem4c  21570  minveclem2  21571  minveclem3b  21573  minveclem4  21577  minveclem6  21579  pmltpclem1  21590  pmltpc  21592  ovollb2lem  21629  ovolctb  21631  ovolunlem1  21638  ovoliunlem1  21643  ovoliunlem2  21644  ovoliun2  21647  ovolshftlem1  21650  ovolscalem1  21654  ovolicc1  21657  ovolicc2lem3  21660  voliunlem2  21691  voliunlem3  21692  ioombl1lem4  21701  uniioovol  21718  uniioombllem2  21722  uniioombllem3  21724  uniioombllem6  21727  volsup2  21744  ismbfd  21777  mbfsup  21801  mbflimsup  21803  itg1climres  21851  mbfi1fseqlem4  21855  itg2lr  21867  itg2leub  21871  itg2seq  21879  itg2monolem1  21887  itg2monolem3  21889  itg2mono  21890  itg2i1fseq2  21893  itg2gt0  21897  itg2cnlem1  21898  itg2cnlem2  21899  itg2cn  21900  iblss  21941  itgless  21953  ibladdlem  21956  iblabsr  21966  iblmulc2  21967  itgabs  21971  ditgeq1  21982  dvferm2lem  22117  rolle  22121  dvlip2  22126  c1liplem1  22127  c1lip1  22128  dvfsumlem2  22158  dvfsumlem4  22160  mdegleb  22194  degltlem1  22202  plyco0  22319  plyeq0lem  22337  coeeq2  22369  dgrle  22370  dgradd2  22394  plydiveu  22423  aareccl  22451  aalioulem2  22458  aaliou3lem7  22474  psercnlem1  22549  pilem2  22576  pilem3  22577  logltb  22707  divlogrlim  22739  logcnlem3  22748  cxpaddlelem  22848  rlimcnp  23018  cxplim  23024  cxploglim  23030  scvxcvx  23038  ftalem1  23069  ftalem2  23070  isppw2  23112  vmappw  23113  sgmnncl  23144  sqff1o  23179  dvdsdivcl  23180  fsumdvdsdiaglem  23182  dvdsppwf1o  23185  dvdsflsumcom  23187  musum  23190  muinv  23192  dvdsmulf1o  23193  vmalelog  23203  vmasum  23214  logfac2  23215  perfectlem2  23228  bcmono  23275  bpos1lem  23280  bposlem9  23290  lgsmod  23319  lgsne0  23331  2sqlem6  23367  2sqlem8  23370  2sqlem10  23372  chtppilim  23383  rpvmasumlem  23395  dchrisumlema  23396  dchrisumlem2  23398  dchrvmasumlem1  23403  dchrvmasumiflem1  23409  dchrisum0flblem1  23416  dchrisum0flblem2  23417  dchrisum0  23428  rplogsum  23435  logsqvma  23450  pntpbnd1  23494  pntpbnd2  23495  pntibndlem3  23500  pntlemj  23511  pntlemi  23512  pntlem3  23517  pnt3  23520  ostth3  23546  lmif  23823  islmib  23825  axlowdim2  23934  axlowdim  23935  axcontlem2  23939  axcontlem3  23940  axcontlem4  23941  axcontlem7  23944  axcontlem9  23946  axcontlem10  23947  axcontlem11  23948  axcontlem12  23949  ebtwntg  23956  usgra1v  24054  usgrafisindb0  24072  usgrafisindb1  24073  cusgra1v  24125  1conngra  24339  clwlkisclwwlklem2fv1  24446  clwlkf1clwwlklem1  24510  isrusgusrgcl  24597  isrgracl  24598  0eusgraiff0rgracl  24605  eupath2  24644  isfrgra  24654  3vfriswmgra  24669  1to2vfriswmgra  24670  vdfrgra0  24686  vdgfrgra0  24687  numclwwlk5  24777  frgraregord013  24783  gxnval  24926  rngosn4  25093  rngoueqz  25096  nmoubi  25351  minvecolem2  25455  minvecolem3  25456  minvecolem4c  25459  minvecolem4  25460  minvecolem5  25461  minvecolem6  25462  htthlem  25498  chlimi  25816  chcompl  25824  hsn0elch  25830  cmbr3  26190  cmcm  26196  cmcm3  26197  lecm  26199  nmopub  26491  nmfnleub  26508  nmopun  26597  nmcexi  26609  cnlnadjlem7  26656  pjnmopi  26731  stle0i  26822  stlesi  26824  stm1i  26826  csmdsymi  26917  cvmd  26919  atcveq0  26931  atcv1  26963  atord  26971  atcvat2  26972  chirred  26978  mdsym  26995  mddmdin0i  27014  cdj1i  27016  fmptcof2  27162  isoun  27180  fcobijfs  27209  lt2addrd  27219  xlt2addrd  27234  xrge0infss  27236  xrofsup  27238  tleile  27299  toslublem  27305  tosglblem  27307  omndadd  27346  xrnarchi  27378  archirng  27382  archiexdiv  27384  archiabl  27392  isarchiofld  27458  ordtrest2NEWlem  27528  ordtconlem1  27530  xrge0iifiso  27541  rge0scvg  27555  gsumesum  27695  esumfsup  27704  esumpinfval  27707  esumpcvgval  27712  esumcvg  27720  sigaclcu  27745  sigaclci  27760  unelsiga  27762  measvun  27808  voliune  27829  volfiniune  27830  oms0  27894  orvcval2  28025  dstfrvel  28040  ballotlemfc0  28059  ballotlemfcc  28060  ballotlemsv  28076  ballotlemsf1o  28080  sgnmulsgn  28116  relexpindlem  28525  rtrclreclem.trans  28532  dfdm5  28771  dfrn5  28772  trpredpred  28876  poseq  28898  wsuclem  28946  nodense  29014  nocvxminlem  29015  nobnddown  29026  nofulllem4  29030  nofulllem5  29031  brpprod  29100  brsset  29104  brbigcup  29113  dffix2  29120  elfuns  29130  brimageg  29142  brdomaing  29150  brrangeg  29151  brimg  29152  brapply  29153  brsuccf  29156  funpartlem  29157  brrestrict  29164  dfrdg4  29165  brofs  29220  btwncomim  29228  btwnintr  29234  btwnexch3  29235  btwnexch2  29238  brifs  29258  brcolinear2  29273  colineardim1  29276  brfs  29294  btwnconn1  29316  segcon2  29320  seglerflx  29327  seglemin  29328  btwnsegle  29332  colinbtwnle  29333  broutsideof2  29337  fvray  29356  lineunray  29362  lineelsb2  29363  linerflx1  29364  fin2solem  29604  fin2so  29605  supaddc  29606  supadd  29607  ltflcei  29608  lxflflp1  29610  heicant  29615  mblfinlem1  29617  mblfinlem2  29618  itg2addnclem  29632  itg2addnclem3  29634  itg2addnc  29635  itg2gt0cn  29636  ibladdnclem  29637  iblmulc2nc  29646  itgabsnc  29650  bddiblnc  29651  ftc1anclem5  29660  ftc1anclem7  29662  ftc1anclem8  29663  ftc1anc  29664  trer  29700  elicc3  29701  finminlem  29702  nn0prpwlem  29706  nn0prpw  29707  indexdom  29817  filbcmb  29823  fdc  29830  prdsbnd  29881  heiborlem3  29901  rrnequiv  29923  prtlem10  30199  lzenom  30296  fphpdo  30344  irrapxlem4  30354  pellexlem6  30363  infmrgelbi  30407  pellfundre  30410  pellfundlb  30413  monotoddzz  30472  zindbi  30475  divalgmodcl  30524  jm2.27  30545  rmydioph  30551  rpnnen3lem  30568  fnwe2lem2  30592  aomclem8  30602  hbtlem5  30672  hbt  30674  phisum  30755  dstregt0  30997  limsupre  31140  icccncfext  31183  cncficcgt0  31184  ioodvbdlimc1lem2  31219  ioodvbdlimc2lem  31221  stoweidlem5  31262  stoweidlem20  31277  stoweidlem26  31283  stoweidlem28  31285  stoweidlem29  31286  stoweidlem34  31291  wallispilem3  31324  stirlinglem13  31343  fourierdlem41  31405  fourierdlem42  31406  fourierdlem51  31415  fourierdlem54  31418  funressnfv  31637  dfdfat2  31640  tz6.12-afv  31682  usgo0s0  31835  usgo1s0  31838  ztprmneprm  31877  ply1mulgsumlem1  31936  ply1mulgsumlem2  31937  lco0  31978  lcoel0  31979  lincsumcl  31982  lincscmcl  31983  lcoss  31987  linindslinci  31999  lindslinindsimp1  32008  linds0  32016  el0ldep  32017  lindsrng01  32019  ldepspr  32024  islindeps2  32034  isldepslvec2  32036  zlmodzxzldep  32063  ldepsnlinc  32067  bnj23  32728  bnj1185  32808  bnj1152  33010  bnj1418  33052  lsatcveq0  33706  lsatcv1  33722  oposlem  33856  opnlen0  33862  lub0N  33863  glb0N  33867  omllaw  33917  cmtbr4N  33929  cvrval  33943  cvrnbtwn  33945  cvrnbtwn2  33949  cvrnbtwn3  33950  cvrcon3b  33951  cvrnbtwn4  33953  atcvreq0  33988  atnle  33991  atlatmstc  33993  cvlexch1  34002  glbconN  34050  hlsuprexch  34054  exatleN  34077  cvratlem  34094  atcvrj0  34101  atcvrj2b  34105  atlelt  34111  cvrat4  34116  3dim1lem5  34139  3dim2  34141  3dim3  34142  ps-2  34151  llni  34181  llnn0  34189  llnle  34191  lplni  34205  lplni2  34210  lplnle  34213  lplnn0N  34220  llncvrlpln  34231  2llnjN  34240  lvoli  34248  lvoli3  34250  lvoli2  34254  lvoln0N  34264  4at  34286  lplncvrlvol  34289  2lplnj  34293  dalemcea  34333  dalem3  34337  psubspi  34420  linepsubN  34425  elpmap  34431  pmapsub  34441  lnatexN  34452  cdlema1N  34464  cdlemb  34467  elpadd  34472  paddvaln0N  34474  paddasslem5  34497  llnexchb2lem  34541  llnexch2N  34543  islhp  34669  lhpat3  34719  4atexlemex2  34744  4atex  34749  4atex2-0aOLDN  34751  4atex2-0cOLDN  34753  lautle  34757  lautcvr  34765  lauteq  34768  ldilval  34786  ltrnu  34794  trlval2  34836  trlne  34858  cdleme0ex1N  34896  cdleme0nex  34963  cdleme18d  34968  cdlemednuN  34973  cdleme25b  35027  cdleme25cv  35031  cdleme27b  35041  cdleme29b  35048  cdleme31sn  35053  cdleme31fv  35063  cdleme31fv2  35066  cdlemefrs29bpre0  35069  cdlemefr29bpre0N  35079  cdlemefr29clN  35080  cdlemefr32fvaN  35082  cdlemefr32fva1  35083  cdlemefs29pre00N  35085  cdlemefs32sn1aw  35087  cdlemefs29bpre0N  35089  cdlemefs29bpre1N  35090  cdlemefs29cpre1N  35091  cdlemefs29clN  35092  cdlemefs32fvaN  35095  cdlemefs32fva1  35096  cdleme41sn3a  35106  cdleme32fva  35110  cdleme32e  35118  cdleme35f  35127  cdleme40v  35142  cdleme42b  35151  trlord  35242  cdlemg1cex  35261  diaval  35706  diaeldm  35710  diaelrnN  35719  cdlemm10N  35792  dibglbN  35840  dicval  35850  dicfnN  35857  dicvalrelN  35859  dihval  35906  dihlsscpre  35908  dihglblem3N  35969  dihmeetlem2N  35973  djhcvat42  36089  taupilemrplb  36643
  Copyright terms: Public domain W3C validator