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

Theorem nfv 1751
Description: If  x is not present in  ph, then  x is not free in  ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfv  |-  F/ x ph
Distinct variable group:    ph, x

Proof of Theorem nfv
StepHypRef Expression
1 ax-5 1748 . 2  |-  ( ph  ->  A. x ph )
21nfi 1670 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-nf 1664
This theorem is referenced by:  nfvd  1752  nexdvOLD  1934  dvelimhw  2010  19.21vOLD  2035  19.23vOLD  2036  pm11.53  2037  19.36vOLD  2038  19.36aivOLD  2039  19.12vv  2040  eeanv  2042  eeeanv  2043  spimv  2062  spimev  2063  chvarv  2067  cbvalv  2076  cbvexv  2077  cbvald  2078  cbval2  2080  cbval2v  2082  cbvex2v  2083  cbvaldva  2084  cbvexdva  2085  axc9lem2  2093  axc16i  2117  dvelimnf  2134  cleljustALT  2161  sbiedv  2202  equsb3lem  2224  equsb3  2225  equsb3ALT  2226  elsb3  2227  elsb4  2228  sbhb  2231  sbnf2  2232  sbcom2  2238  sbcom4  2239  dfsb7  2248  sbid2v  2250  sbel2x  2252  sbco4lem  2258  sbco4  2259  2sb8e  2260  exsb  2261  euf  2272  mo2  2273  nfeud2  2276  eubidv  2284  mobidv  2285  sb8eu  2297  euexALT  2305  euorv  2307  sbmo  2309  mo4f  2310  mo4  2311  moanimv  2325  euanv  2328  moexexv  2336  2mo  2345  2moOLD  2346  2mos  2347  2eu6  2354  bm1.1  2403  bm1.1OLD  2404  cleqh  2535  eqsb3lem  2539  eqsb3  2540  clelsb3  2541  abbiOLD  2552  abbidv  2556  cbvabv  2563  clelab  2564  clelabOLD  2565  nfcjust  2569  nfcv  2582  nfeqd  2589  nfeld  2590  nfabd2  2603  dvelimdc  2605  cleqfOLD  2610  sbabel  2614  sbabelOLD  2615  r19.21vOLD  2829  ralimdvaOLD  2832  ralrimivOLD  2836  ralrimdvOLD  2840  ralbidvaOLD  2860  ralbidvOLD  2863  2ralbida  2864  2ralbidvaOLD  2866  reximdvaiOLD  2896  r19.23vOLD  2904  rexlimivOLD  2910  rexlimdvOLD  2914  rexbidvaALT  2935  rexbidvALT  2938  r19.29af  2966  r19.29an  2967  r19.29a  2968  r19.37v  2976  reean  2993  reeanv  2994  reubidva  3010  rmobidva  3015  cbvralf  3047  cbvreu  3051  cbvralv  3053  cbvrexv  3054  cbvreuv  3055  cbvrmov  3056  cbvralsv  3064  cbvrexsv  3065  sbralie  3066  cbvrab  3076  cbvrabv  3077  issetf  3083  ceqsalv  3106  ceqsralv  3107  ceqsexv  3115  ceqsex2  3116  ceqsex2v  3117  vtocld  3128  vtocl  3130  vtoclg  3136  vtocl2g  3140  vtoclga  3142  vtocl2gaf  3143  vtocl2ga  3144  vtocl3gaf  3145  vtocl3ga  3146  spcimdv  3160  spcgv  3163  spcegv  3164  rspct  3172  rspc  3173  rspce  3174  rspcv  3175  rspcev  3179  rspc2v  3188  eqvincf  3196  ceqsexgv  3201  elabgt  3212  elab  3215  elabg  3216  elab3g  3221  elrab3t  3225  elrab  3226  ralab2  3233  rexab2  3235  mob2  3248  mob  3250  reu2  3256  reu2eqd  3265  nfcdeq  3293  sbcco  3319  sbcco2  3320  cbvsbcv  3326  sbcieg  3329  sbcie2g  3330  sbcied  3333  elrabsf  3335  sbcbidv  3351  sbcg  3362  sbc2iegf  3363  sbc2ie  3364  rmo2  3385  rmo3  3387  nfcsb1d  3406  nfcsbd  3409  csbiebt  3412  csbied  3419  csbie2t  3421  cbvralcsf  3424  cbvreucsf  3426  cbvrabcsf  3427  cbvralv2  3428  cbvrexv2  3429  dfss2f  3452  uniiunlem  3546  rspn0  3771  csbeq2dv  3806  sbcnestg  3811  sbnfc2  3821  sbss  3904  nfifd  3934  rabsnifsb  4062  euabsn  4066  nfuni  4219  nfunid  4220  eluniab  4224  nfint  4259  elintab  4260  rabasiun  4297  iineq2dv  4316  disjiun  4408  disjxun  4415  opabbidv  4480  nfopab  4482  cbvopab  4485  cbvopabv  4486  cbvopab1  4487  cbvopab2  4488  cbvopab1s  4489  cbvopab1v  4490  mpteq12f  4493  mpteq2dva  4503  cbvmptf  4507  cbvmpt  4508  axrep1  4530  axrep2  4531  axrep3  4532  axrep4  4533  axrep5  4534  zfrepclf  4535  axsep  4538  zfnuleu  4544  reusv2lem2  4618  reusv2lem3  4619  reusv2lem4  4620  reusv2  4622  reusv3  4624  alxfr  4626  ralxfrALT  4632  copsex2t  4699  copsex2g  4700  opelopabaf  4736  nfso  4772  pofun  4782  nffr  4819  opeliunxp  4897  opeliunxp2  4984  ralxpf  4992  dfdmf  5039  dfrnf  5084  elrnmpt1  5094  asymref2  5228  intirr  5229  wfisg  5425  wfis2g  5429  nfiotad  5559  cbviota  5561  cbviotav  5562  sb8iota  5563  iota2d  5581  iota2  5582  dffun6f  5606  fun11  5657  imadif  5667  funimaexg  5669  isarep1  5671  isarep2  5672  fv3  5885  tz6.12f  5890  tz6.12c  5891  opabiotafun  5933  funfv2f  5941  fvmptdf  5968  fvmptdv  5969  fvmptt  5972  fvopab5  5980  eqfnfv2f  5986  ralrnmpt  6037  f1ompt  6050  ffnfv  6055  ffnfvf  6056  fmptco  6062  elabrex  6154  dff13f  6166  fsnex  6187  fliftfun  6211  cbvriota  6268  cbvriotav  6269  riota2  6280  riota5f  6282  oprabv  6344  nfoprab  6348  oprabbidv  6350  mpt2eq123  6355  cbvoprab1  6368  cbvoprab2  6369  cbvoprab12  6370  cbvoprab12v  6371  cbvoprab3  6372  cbvoprab3v  6373  cbvmpt2x  6374  ralrnmpt2  6416  ovmpt2dx  6428  ovmpt2df  6433  ovmpt2dv  6434  ov3  6438  ovmpt3rab1  6530  ofrfval2  6554  onminex  6639  tfis  6686  tfis2  6688  tfisi  6690  tfinds  6691  tfindes  6694  peano5  6721  findes  6728  fun11iun  6758  abrexex2g  6775  opabex3d  6776  opabex3  6777  abrexex2  6779  dfoprab4f  6856  fmpt2x  6864  offval22  6877  ovmptss  6879  tposoprab  7008  fvmpt2curryd  7017  nfwrecs  7029  tfr3  7116  nfrdg  7131  tz7.48-1  7159  tz7.49  7161  eqerlem  7394  erovlem  7458  mptelixpg  7558  boxcutc  7564  dom2lem  7607  xpf1o  7731  mapxpen  7735  nneneq  7752  pssnn  7787  findcard2  7808  ac6sfi  7812  fiint  7845  indexfi  7879  wdom2d  8086  ixpiunwdom  8097  cantnflem1  8184  r1val1  8247  rankuni2b  8314  scottexs  8348  scott0s  8349  dfac8clem  8452  acni2  8466  aceq1  8537  dfac5lem5  8547  kmlem15  8583  infpssrlem4  8725  fin23lem27  8747  hsmexlem2  8846  hsmexlem4  8848  axcc3  8857  domtriomlem  8861  axdc3lem2  8870  axdc3lem4  8872  axdc4lem  8874  ac6num  8898  ac6c4  8900  zorn2lem4  8918  zorn2lem5  8919  iunfo  8953  iundom2g  8954  uniimadomf  8959  konigthlem  8982  axrepndlem2  9007  axunnd  9010  axpowndlem2  9012  axpowndlem4  9014  axregndlem2  9017  axacndlem5  9025  zfcndrep  9028  zfcndinf  9032  pwfseqlem4a  9075  pwfseqlem4  9076  tskuni  9197  gruiin  9224  reclem2pr  9462  dedekind  9786  dedekindle  9787  fimaxre3  10542  nn0ind-raph  11024  uzind4s  11208  nnwof  11214  lbzbi  11241  fzrevral  11866  rabssnn0fi  12184  fsuppmapnn0fiublem  12188  fsuppmapnn0fiub  12189  fsuppmapnn0fiubex  12190  seqof2  12257  cotr2g  13008  rlim2  13527  ello1mpt  13552  climeu  13586  o1compt  13618  summolem2a  13748  zsum  13751  sumss  13757  sumss2  13759  fsumcvg2  13760  fsum2dlem  13798  fsum00  13825  o1fsum  13840  nfcprod1  13931  nfcprod  13932  prodmolem2a  13955  zprod  13958  fprod  13962  fprodntriv  13963  prodss  13968  fprodn0  14000  fprod2dlem  14001  fprodsplitf  14009  fprodsplit1f  14011  fprodle  14017  lcmfunsnlem1  14570  lcmfunsnlem2lem1  14571  lcmfunsnlem2  14573  prmind2  14595  coprmprod  14638  coprmproddvdslem  14639  iserodd  14737  pcmpt  14789  pcmptdvds  14791  prmolefac  14956  prmorlefacOLD  14970  mreexexd  15498  catpropd  15558  invfuc  15823  natpropd  15825  fucpropd  15826  initoeu2  15855  acsmapd  16368  gsumsnd  17513  gsumsnf  17514  gsumunsnfd  17517  gsummptf1o  17523  gsummpt1n0  17525  gsum2d2lem  17533  gsumcom2  17535  gsummptnn0fz  17543  gsummptnn0fzv  17544  dprdwdOLD  17572  dprd2d2  17605  gsummoncoe1  18826  gsumply1eq  18827  mdetralt2  19558  mdetunilem2  19562  madugsum  19592  gsummatr01lem4  19607  cpmatmcllem  19666  pmatcollpwfi  19730  cayleyhamilton1  19840  neiptopnei  20072  neiptopreu  20073  neitr  20120  fiuncmp  20343  iunconlem  20366  iuncon  20367  2ndcdisj  20395  dissnlocfin  20468  elptr2  20513  ptbasfi  20520  ptcld  20552  ptcldmpt  20553  ptclsg  20554  ptcnplem  20560  ptcnp  20561  cnmpt11  20602  cnmpt21  20610  cnmptcom  20617  imasnopn  20629  imasncld  20630  imasncls  20631  xkocnv  20753  elmptrab  20766  isfildlem  20796  alexsubALTlem3  20988  cnextfvval  21004  utopsnneiplem  21186  isucn2  21218  cfilucfil  21498  blval2  21501  restmetu  21509  ovoliunlem3  22331  ovoliun  22332  ovoliun2  22333  ovoliunnul  22334  finiunmbl  22371  volfiniun  22374  iundisj  22375  iunmbl  22380  voliun  22381  iunmbl2  22384  mbfeqalem  22472  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  mbflim  22500  itg2splitlem  22580  itg2split  22581  isibl2  22598  cbvitg  22607  itgeqa  22645  itgss3  22646  itgfsum  22658  itgabs  22666  itggt0  22673  itgcn  22674  limcmpt  22712  limciun  22723  dvmptfsum  22801  dvlipcn  22820  dvfsumlem2  22853  dvfsumlem4  22855  dvfsumrlim  22857  dvfsum2  22860  itgsubst  22875  coeeq2  23061  dgrle  23062  ulmss  23214  leibpi  23730  rlimcnp  23753  rlimcnp2  23754  o1cxp  23762  lgamgulmlem2  23817  lgamgulmlem6  23821  fsumdvdscom  23974  lgseisenlem2  24138  dchrisumlema  24186  dchrisumlem2  24188  dchrisumlem3  24189  istrkg2ld  24368  mptelee  24768  ex-natded9.26  25711  isch3  26726  atom1d  27838  chirred  27880  spc2ed  27938  vtocl2d  27941  19.9d2r  27945  rspcda  27946  clelsb3f  27948  mo5f  27952  rmoeq  27955  rmo4fOLD  27964  rmo4f  27965  foresf1o  27972  elabreximdv  27978  rabss3d  27981  iuninc  28012  cbvdisjf  28018  disjorf  28025  disjabrex  28028  iundisjf  28035  disjunsn  28040  dfrel4  28044  brabgaf  28052  elsnxp  28060  ac6sf2  28063  dfimafnf  28070  suppss2fOLD  28074  fimarab  28081  mpteq12df  28093  feqmptdf  28095  fmptcof2  28096  acunirnmpt2  28099  acunirnmpt2f  28100  aciunf1lem  28101  aciunf1  28102  ofpreima  28105  funcnvmptOLD  28107  funcnv5mpt  28109  funcnv4mpt  28110  padct  28147  cnvoprab  28148  f1od2  28149  fpwrelmap  28158  xrofsup  28186  iundisjfi  28205  nnindf  28217  nn0min  28219  2sqmo  28245  gsummpt2d  28379  isarchiofld  28416  reff  28502  locfinreflem  28503  cmpcref  28513  ordtconlem1  28566  qqhval2  28622  esumeq12dva  28689  esumeq2dv  28695  esumrnmpt  28709  esumpad  28712  esumpad2  28713  esumadd  28714  gsumesum  28716  esumlub  28717  esumsnf  28721  esumpr  28723  esumrnmpt2  28725  esumfzf  28726  esumfsup  28727  esumpcvgval  28735  esumpmono  28736  esumcocn  28737  hasheuni  28742  esumcvg  28743  esumgect  28747  esum2dlem  28749  esum2d  28750  esumiun  28751  ldsysgenld  28818  sigapildsyslem  28819  sigapildsys  28820  ldgenpisyslem1  28821  fiunelros  28832  measvunilem  28870  measvunilem0  28871  measvuni  28872  measiuns  28875  measiun  28876  measinblem  28878  voliune  28888  volfiniune  28889  volmeas  28890  ddemeas  28895  oms0  28955  omssubadd  28958  carsgclctunlem1  28975  carsggect  28976  omsmeas  28981  eulerpartlemgvv  29032  dstrvprob  29127  ballotlemodife  29153  bnj919  29363  bnj1146  29388  bnj1379  29427  bnj1385  29429  bnj1400  29432  bnj1476  29443  bnj1534  29449  bnj1542  29453  bnj110  29454  bnj121  29466  bnj124  29467  bnj130  29470  bnj207  29477  bnj571  29502  bnj605  29503  bnj580  29509  bnj607  29512  bnj611  29514  bnj873  29520  bnj849  29521  bnj900  29525  bnj916  29529  bnj1000  29537  bnj964  29539  bnj981  29546  bnj985  29549  bnj1014  29556  bnj1123  29580  bnj1128  29584  bnj1228  29605  bnj1204  29606  bnj1279  29612  bnj1307  29617  bnj1321  29621  bnj1388  29627  bnj1398  29628  bnj1408  29630  bnj1417  29635  bnj1444  29637  bnj1445  29638  bnj1446  29639  bnj1449  29642  bnj1467  29648  bnj1489  29650  bnj1312  29652  bnj1497  29654  bnj1518  29658  bnj1525  29663  bnj1529  29664  cvmcov  29771  untsucf  30122  mpteq12d  30196  setinds2  30210  dfon2lem1  30213  dfon2lem3  30215  trpredmintr  30256  frinsg  30267  frins2g  30271  frins2  30272  finminlem  30756  bj-nexdvt  31028  bj-spimvv  31059  bj-spimevv  31060  bj-chvarvv  31064  bj-cbv3v2  31066  bj-cbvalvv  31075  bj-cbvexvv  31076  bj-cbvaldv  31077  bj-cbval2v  31079  bj-cbval2vv  31081  bj-cbvex2vv  31082  bj-cbvaldvav  31083  bj-cbvexdvav  31084  bj-drnf2v  31106  bj-abbi  31138  bj-abbidv  31142  bj-axrep1  31151  bj-axrep2  31152  bj-axrep3  31153  bj-axrep4  31154  bj-axrep5  31155  bj-axsep  31156  ax11-pm2  31186  bj-mo3OLD  31195  bj-clelsb3  31205  bj-nfcjust  31207  bj-ceqsalv  31240  bj-vtocl  31263  bj-inrab2  31278  mptsnunlem  31471  exlimim  31475  exellim  31478  topdifinfindis  31480  topdifinffinlem  31481  icorempt2  31485  isbasisrelowllem1  31489  isbasisrelowllem2  31490  relowlssretop  31497  wl-equsb3  31588  wl-euequ1f  31607  wl-sb8eut  31610  phpreu  31633  ptrest  31643  ptrecube  31644  poimirlem2  31646  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  heicant  31679  mbfposadd  31692  itgabsnc  31715  itggt0cn  31718  ftc1anclem5  31725  upixp  31760  indexa  31764  indexdom  31765  filbcmb  31771  sdclem2  31775  sdclem1  31776  fdc1  31779  totbndbnd  31825  sbcalf  32056  sbcexf  32057  scottexf  32115  scott0f  32116  prtlem5  32136  fsumshftd  32232  fsumshftdOLD  32233  riotasv2d  32238  riotasv2s  32239  riotasv3d  32241  glbconxN  32652  pmapglbx  33043  pmapglb2xN  33046  cdleme26ee  33636  cdleme31sn  33656  cdleme31sn1  33657  cdlemefr29exN  33678  cdlemefs32sn1aw  33690  cdleme43fsv1snlem  33696  cdleme41sn3a  33709  cdleme32fva  33713  cdleme32d  33720  cdleme32f  33722  cdleme40m  33743  cdleme40n  33744  cdleme42b  33754  cdlemk36  34189  cdlemk38  34191  cdlemkid  34212  cdlemk19x  34219  cdlemk11t  34222  dihvalcqpre  34512  mapdheq  35005  hdmap1eq  35079  hdmapval2lem  35111  mzpexpmpt  35296  eq0rabdioph  35328  rexrabdioph  35346  rexfrabdioph  35347  elnn0rabdioph  35355  dvdsrabdioph  35362  fphpd  35368  monotuz  35499  monotoddzz  35501  oddcomabszz  35502  setindtr  35589  dford4  35594  wdom2d2  35600  aomclem6  35627  aomclem8  35629  flcidc  35743  areaquad  35804  ss2iundv  35895  cbviuneq12dv  35897  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  aaanv  36379  pm11.57  36380  pm11.58  36381  pm11.59  36382  pm11.71  36388  pm13.192  36402  pm14.12  36413  ssralv2  36529  tratrb  36538  iunconlem2  36976  evth2f  36980  elunif  36981  fvelrnbf  36983  evthf  36992  fnchoice  36994  sumpair  37000  rfcnnnub  37001  refsum2cn  37003  elabrexg  37014  uzwo4  37037  fiiuncl  37052  fiunicl  37054  suprnmpt  37065  dffo3f  37077  disjf1  37084  wessf1ornlem  37086  disjrnmpt2  37090  disjf1o  37093  fompt  37094  disjinfi  37095  upbdrech  37136  ssfiunibd  37140  supxrgere  37169  iuneqfzuzlem  37170  supxrgelem  37173  supxrge  37174  suplesup  37175  iccshift  37208  iooshift  37212  fsumclf  37224  fsumsplitf  37225  fsummulc1f  37226  fsumnncl  37229  fsumsplit1  37230  fsumf1of  37232  fsumiunss  37233  fmul01  37234  fmuldfeqlem1  37236  fmuldfeq  37237  fmul01lt1lem1  37238  fmul01lt1lem2  37239  fmul01lt1  37240  infrglbOLD  37245  fprodsplit1  37249  fprodexp  37250  fprodabs2  37251  mccllem  37253  mccl  37254  climexp  37259  climsuse  37263  climrecf  37264  climinff  37266  climinffOLD  37267  climaddf  37271  mullimc  37272  ellimcabssub0  37273  islptre  37275  climf  37278  mullimcf  37279  rexlim2d  37281  idlimc  37282  limcperiod  37284  limcrecl  37285  sumnnodd  37286  islpcn  37295  limsupre  37297  limsupreOLD  37298  limcleqr  37301  neglimc  37304  addlimc  37305  0ellimcdiv  37306  limclner  37308  cncfshift  37327  icccncfext  37341  cncficcgt0  37342  cncfiooicclem1  37347  cncfiooicc  37348  cncfioobd  37351  fprodcncf  37355  dvmptmulf  37385  dvnmptdivc  37386  dvnmul  37391  dvmptfprodlem  37392  dvmptfprod  37393  dvnprodlem1  37394  dvnprodlem2  37395  iblsplitf  37420  iblspltprt  37423  itgioocnicc  37427  iblcncfioo  37428  itgspltprt  37429  itgperiod  37431  stoweidlem3  37436  stoweidlem14  37447  stoweidlem17  37450  stoweidlem19  37452  stoweidlem20  37453  stoweidlem26  37459  stoweidlem27  37460  stoweidlem28  37461  stoweidlem29  37462  stoweidlem29OLD  37463  stoweidlem31  37465  stoweidlem34  37468  stoweidlem35  37469  stoweidlem36  37470  stoweidlem39  37473  stoweidlem42  37476  stoweidlem43  37477  stoweidlem44  37478  stoweidlem46  37480  stoweidlem48  37482  stoweidlem49  37483  stoweidlem50  37484  stoweidlem51  37485  stoweidlem52  37486  stoweidlem53  37487  stoweidlem54  37488  stoweidlem56  37490  stoweidlem57  37491  stoweidlem59  37493  stoweidlem60  37494  stoweidlem61  37495  stoweidlem62  37496  stoweidlem62OLD  37497  stoweid  37498  wallispilem3  37502  stirlinglem13  37521  stirling  37524  fourierdlem16  37558  fourierdlem21  37563  fourierdlem22  37564  fourierdlem31  37573  fourierdlem39  37581  fourierdlem48  37590  fourierdlem51  37593  fourierdlem53  37595  fourierdlem68  37610  fourierdlem69  37611  fourierdlem71  37613  fourierdlem73  37615  fourierdlem77  37619  fourierdlem80  37622  fourierdlem81  37623  fourierdlem82  37624  fourierdlem83  37625  fourierdlem86  37628  fourierdlem87  37629  fourierdlem89  37631  fourierdlem91  37633  fourierdlem93  37635  fourierdlem94  37636  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  fourierdlem113  37655  elaa2  37670  etransclem18  37688  etransclem22  37692  etransclem23  37693  etransclem32  37702  etransclem35  37705  etransclem44  37714  etransclem46  37716  etransclem48  37718  intsaluni  37739  sge00  37756  sge0revalmpt  37758  sge0sn  37759  sge0f1o  37762  sge0gerp  37775  sge0pnffigt  37776  sge0lefi  37778  sge0ltfirp  37780  sge0resrnlem  37783  sge0resplit  37786  sge0lempt  37790  sge0iunmptlemfi  37793  sge0p1  37794  sge0iunmptlemre  37795  sge0fodjrnlem  37796  sge0iunmpt  37798  iundjiun  37811  meadjiunlem  37816  meadjiun  37817  ismeannd  37818  caragenfiiuncl  37849  omeiunltfirp  37853  carageniuncllem1  37855  carageniuncllem2  37856  caratheodorylem2  37861  rexsb  37993  rmoanim  38004  2reu4a  38014  ffnafv  38076  iccelpart  38150  iccpartdisj  38154  2zrngagrp  38714  2zrngmmgm  38717  opeliun2xp  38887  cbvmpt2x2  38890  ovmpt2rdx  38894  aacllem  39314
  Copyright terms: Public domain W3C validator