Theorem fveq2i 6923

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fveq2i	⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fveq2 6920	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  fveq12i  6926  ot1stg  8044  ot2ndg  8045  ot3rdg  8046  wfrlem5OLD  8369  wfrlem14OLD  8378  tfr2a  8451  rdgsucmptf  8484  rdgsucmptnf  8485  rdg0n  8490  frsucmpt  8494  frsucmptn  8495  infiso  9577  inf3lemc  9695  cantnf  9762  wemapwe  9766  cnfcom2lem  9770  cnfcom2  9771  cnfcom3lem  9772  r1sucg  9838  rankprb  9920  rankopb  9921  ranksuc  9934  rankmapu  9947  cardiun  10051  alephsuc  10137  alephcard  10139  alephfplem2  10174  ackbij1lem8  10295  ackbij1lem13  10300  ackbij1lem14  10301  ackbij2lem2  10308  infpssrlem2  10373  fin23lem34  10415  fin23lem35  10416  aleph1  10640  pwcfsdom  10652  cfpwsdom  10653  alephom  10654  rankcf  10846  addpqnq  11007  mulpqnq  11010  addcomnq  11020  mulcomnq  11022  addclprlem2  11086  infrenegsup  12278  fseq1p1m1  13658  fldiv4p1lem1div2  13886  om2uzrdg  14007  uzrdgsuci  14011  fzennn  14019  axdc4uzlem  14034  seqp1d  14069  seqf1olem2  14093  facp1  14327  fac2  14328  fac3  14329  fac4  14330  4bc2eq6  14378  hashcard  14404  hasheq0  14412  hashun2  14432  hashun3  14433  hashprg  14444  hashprb  14446  hashprdifel  14447  hashp1i  14452  pr0hash2ex  14457  hashdif  14462  hashunlei  14474  hashfzo  14478  hashxplem  14482  hashfun  14486  hashimarn  14489  hashbclem  14501  hashbc  14502  hashf1lem2  14505  hashtpg  14534  ccatalpha  14641  s1len  14654  ccat2s1p2  14678  revs1  14813  cats1len  14909  lsws2  14953  lsws3  14954  lsws4  14955  rei  15205  imi  15206  sqrt1  15320  sqrt4  15321  sqrt9  15322  abs0  15334  absi  15335  sqreulem  15408  fsumabs  15849  fsumrelem  15855  o1fsum  15861  hashrabrex  15873  hashuni  15874  incexclem  15884  incexc  15885  isumnn0nn  15890  fprodefsum  16143  efsep  16158  sin0  16197  cos0  16198  ef01bndlem  16232  cos2bnd  16236  sin4lt0  16243  ruclem6  16283  aleph1re  16293  pwp1fsum  16439  m1bits  16486  sadcaddlem  16503  sadaddlem  16512  sadeq  16518  algrp1  16621  eucalg  16634  prmind2  16732  dfphi2  16821  phiprmpw  16823  phimullem  16826  pockthlem  16952  pockthg  16953  prmunb  16961  prmreclem4  16966  vdwap1  17024  vdwlem12  17039  prmo2  17087  prmo3  17088  prmgaplem7  17104  prmo4  17175  prmo5  17176  prmo6  17177  imasvsca  17580  mreexdomd  17707  isoval  17826  yonedalem21  18343  yonedalem22  18348  oduleval  18359  odubas  18361  odubasOLD  18362  joincomALT  18471  meetcomALT  18473  lubsn  18552  isacs5lem  18615  acsmapd  18624  efmnd1hash  18927  efmnd1bas  18928  efmnd2hash  18929  ressmulgnnd  19118  oppgplusfval  19388  setsplusg  19390  oppglemOLD  19391  symgbas  19413  symghash  19419  symgplusg  19424  symg1hash  19431  symg2hash  19433  symgtset  19441  symggen  19512  psgnsn  19562  psgnprfval1  19564  psgnprfval2  19565  odngen  19619  sylow1lem1  19640  efgs1b  19778  efgsfo  19781  efgredlemg  19784  efgredlemd  19786  frgpuplem  19814  gsumzmhm  19979  gsumzinv  19987  dprd2da  20086  dmdprdsplit2lem  20089  pgpfaclem1  20125  mgpplusg  20165  mgplemOLD  20166  ringidval  20210  opprmulfval  20362  opprlem  20365  opprlemOLD  20366  isrhm2d  20513  rhm1  20515  rhmopp  20535  cntzsubrng  20593  rhmsubclem3  20709  rhmsubclem4  20710  subdrgint  20826  rmodislmod  20950  rmodislmodOLD  20951  lspprid2  21019  lsmpr  21111  lsppr  21115  lspsntri  21119  lbspropd  21121  lspexchn2  21156  lspindp2l  21159  lspindp2  21160  lspsnat  21170  lsppratlem1  21172  lsppratlem3  21174  lsppratlem4  21175  lidlrsppropd  21277  zrhpsgnodpm  21633  psgnfix1  21639  psgnfix2  21640  psgndiflemB  21641  dsmmbas2  21780  dsmmelbas  21782  dsmmsubg  21786  frlmip  21821  islinds2  21856  lindsind2  21862  lindfmm  21870  islindf4  21881  assamulgscmlem2  21943  evlsval  22133  selvval  22162  psropprmul  22260  ply1sca2  22276  ply1mpl0  22279  ply1mpl1  22281  coe1fzgsumd  22329  ply1fermltlchr  22337  evls1var  22363  evl1gsumd  22382  evl1varpw  22386  evl1varpwval  22387  evl1scvarpw  22388  mat1bas  22476  mat0dim0  22494  mat0dimid  22495  mat0dimscm  22496  mat0dimcrng  22497  mat1rhmelval  22507  dmatval  22519  scmatval  22531  mat1scmat  22566  1mavmul  22575  marrepfval  22587  marepvfval  22592  ma1repvcl  22597  ma1repveval  22598  submafval  22606  mdetfval1  22617  mdetralt  22635  mdetunilem7  22645  m2detleiblem3  22656  m2detleiblem4  22657  madufval  22664  maducoeval2  22667  madugsum  22670  minmar1fval  22673  cramerimplem1  22710  cramer0  22717  pmatcoe1fsupp  22728  cpmat  22736  mat2pmatfval  22750  mat2pmatmul  22758  idmatidpmat  22764  m2cpminv0  22788  pmatcollpwfi  22809  pmatcollpw3fi1lem1  22813  pm2mpval  22822  chpmatval2  22860  cpmidpmat  22900  cayleyhamilton1  22919  sn0cld  23119  lpdifsn  23172  restcls  23210  restntr  23211  ordtrest2  23233  leordtval  23242  pttoponconst  23626  ptclsg  23644  xkoptsub  23683  xkofvcn  23713  tgqtop  23741  hmeocls  23797  hmeontr  23798  ptcmpfi  23842  ptcmplem1  24081  tmdgsum  24124  utop2nei  24280  cuspcvg  24331  iscusp2  24332  cnextucn  24333  comet  24547  nrmmetd  24608  isngp3  24632  ngpds  24638  tngnm  24693  cnmetdval  24812  qdensere2  24838  tgioo3  24846  cnmpopc  24974  cnheibor  25006  htpyco2  25030  phtpyco2  25041  pco0  25066  pi1xfrcnv  25109  cnrbas  25194  cncvs  25197  cnnm  25213  ipcau2  25287  cfilfcls  25327  cncmet  25375  reust  25434  rrxprds  25442  rrxsca  25449  ehleudis  25471  ehleudisval  25472  pjthlem1  25490  ovolunlem1a  25550  ovolfiniun  25555  ovoliunlem2  25557  ovoliunlem3  25558  ovoliun  25559  ovolicc1  25570  ismbl2  25581  unmbl  25591  volinun  25600  volfiniun  25601  voliunlem1  25604  voliunlem2  25605  ioorinv  25630  mbfimaopnlem  25709  itg2cnlem2  25817  itg2cn  25818  dfitg  25824  cbvitgv  25832  itg0  25835  iblre  25849  itgreval  25852  itgitg2  25862  iblconst  25873  itgconst  25874  itgcn  25900  limcflflem  25935  dvn1  25982  dvlipcn  26053  c1lip2  26057  dvcnvrelem2  26077  ply1divalg2  26198  ply1remlem  26224  dgr0  26322  elqaalem2  26380  dvradcnv  26482  pserdvlem2  26490  pserdv2  26492  abelthlem6  26498  abelthlem9  26502  sinhalfpilem  26523  cospi  26532  sincos4thpi  26573  sincos6thpi  26576  sincos3rdpi  26577  pige3ALT  26580  sinkpi  26582  eflog  26636  logfac  26661  logdmopn  26709  logtayl  26720  cxpcn3  26809  root1eq1  26816  cxpeq  26818  logbleb  26844  logblt  26845  sqrt2cxp2logb9e3  26860  ang180lem1  26870  ang180lem2  26871  ang180lem4  26873  lawcos  26877  1cubrlem  26902  asin1  26955  atan0  26969  atan1  26989  log2cnv  27005  birthdaylem2  27013  lgamgulmlem2  27091  gam1  27126  ftalem3  27136  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  ppi1  27225  ppi1i  27229  ppi2i  27230  cht2  27233  cht3  27234  ppiub  27266  chtub  27274  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsval2lem  27369  lgsqrlem1  27408  lgsqrlem4  27411  lgsquadlem2  27443  chebbnd1  27534  rplogsumlem1  27546  rplogsumlem2  27547  dchrisum0flb  27572  mulog2sumlem2  27597  pntpbnd1a  27647  pntlemf  27667  nosepne  27743  noinfbnd2lem1  27793  bday0s  27891  bday1s  27894  left0s  27949  right0s  27950  left1s  27951  right1s  27952  precsexlem1  28249  precsexlem2  28250  zseo  28424  cchhllem  28919  cchhllemOLD  28920  axlowdimlem17  28991  graop  29064  setsiedg  29071  vtxvalsnop  29076  iedgvalsnop  29077  usgrexmpllem  29295  uhgrspan1lem2  29336  uhgrspan1lem3  29337  upgrres1lem2  29346  upgrres1lem3  29347  structtocusgr  29481  cusgrsizeinds  29488  cusgrsize  29490  vtxdg0e  29510  uspgrloopvtx  29551  uspgrloopiedg  29553  uspgrloopedg  29554  umgr2v2evtx  29557  umgr2v2eiedg  29559  vtxdginducedm1lem1  29575  vtxdginducedm1  29579  vtxdginducedm1fi  29580  finsumvtxdg2ssteplem1  29581  finsumvtxdg2ssteplem2  29582  finsumvtxdg2ssteplem3  29583  finsumvtxdg2ssteplem4  29584  finsumvtxdg2sstep  29585  finsumvtxdg2size  29586  wlkres  29706  wlkp1lem2  29710  trlreslem  29735  clwlkcompbp  29818  crctcshlem2  29851  crctcshwlkn0  29854  2wlkdlem1  29958  2wlkdlem2  29959  2wlkdlem4  29961  2pthdlem1  29963  2wlkond  29970  2pthd  29973  umgr2adedgwlk  29978  clwwlknclwwlkdifnum  30012  clwwlkccatlem  30021  clwlkclwwlkfo  30041  clwlknf1oclwwlkn  30116  clwwlknon2num  30137  0wlkon  30152  0clwlk  30162  0cycl  30166  1pthdlem1  30167  1pthdlem2  30168  1wlkdlem1  30169  1wlkdlem4  30172  1pthond  30176  lp1cycl  30184  wlk2v2elem2  30188  wlk2v2e  30189  3wlkdlem1  30191  3wlkdlem2  30192  3wlkdlem4  30194  3pthdlem1  30196  3wlkond  30203  3pthd  30206  3cycld  30210  3cyclpd  30211  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2eucrct  30249  eupthvdres  30267  eupth2lem3  30268  eucrct2eupth  30277  konigsbergvtx  30278  konigsbergiedg  30279  konigsberg  30289  2clwwlk2  30380  numclwlk1lem1  30401  numclwlk1  30403  numclwwlkqhash  30407  frgrreg  30426  ex-co  30470  ex-ceil  30480  ex-fac  30483  ex-hash  30485  ex-sqrt  30486  ex-prmo  30491  0vfval  30638  nvvop  30641  vsfval  30665  cnnvg  30710  cnnvs  30712  cnnvnm  30713  imsdval  30718  ipidsq  30742  nmblolbii  30831  blocnilem  30836  ip0i  30857  ip1ilem  30858  ipasslem10  30871  siilem1  30883  cnbn  30901  h2hva  31006  h2hsm  31007  h2hnm  31008  axhfvadd-zf  31014  axhvcom-zf  31015  axhvass-zf  31016  axhv0cl-zf  31017  axhvaddid-zf  31018  axhfvmul-zf  31019  axhvmulid-zf  31020  axhvmulass-zf  31021  axhvdistr1-zf  31022  axhvdistr2-zf  31023  axhvmul0-zf  31024  axhfi-zf  31025  axhis1-zf  31026  axhis2-zf  31027  axhis3-zf  31028  axhis4-zf  31029  axhcompl-zf  31030  norm-iii-i  31171  normsubi  31173  norm3difi  31179  normpar2i  31188  hh0v  31200  hhssva  31289  hhsssm  31290  hhssnm  31291  hhshsslem1  31299  hhsscms  31310  choc1  31359  shjcom  31390  pjhthlem1  31423  pjoc2i  31470  shs0i  31481  chj0i  31487  chdmj1i  31513  chjassi  31518  spansn0  31573  spanpr  31612  qlaxr4i  31666  pjadjii  31706  pjaddii  31707  pjmulii  31709  pjsubii  31710  pjcji  31716  pjnormi  31753  pjpythi  31754  ho0val  31782  lnop0  31998  lnophmlem2  32049  nmbdoplbi  32056  nmcopexi  32059  lnfn0i  32074  nmcfnexi  32083  nmopadji  32122  nmoptri2i  32131  nmopcoadj2i  32134  unierri  32136  branmfn  32137  pjbdlni  32181  pjclem2  32228  sto1i  32268  stm1ri  32276  st0  32281  hstrlem3a  32292  hstrlem4  32294  golem1  32303  superpos  32386  shatomistici  32393  iuninc  32583  hashunif  32813  pfxlsw2ccat  32917  chnub  32984  pmtrprfv2  33081  psgnfzto1st  33098  cyc2fv1  33114  cycpmco2lem4  33122  cycpmco2lem7  33125  cycpmco2  33126  cyc3fv1  33130  cyc3fv2  33131  cycpmrn  33136  cyc3genpmlem  33144  rlocval  33231  primefldchr  33268  xrge0slmod  33341  imaslmhm  33350  zringfrac  33547  evl1deg2  33567  evl1deg3  33568  lmimdim  33616  rlmdim  33622  rgmoddimOLD  33623  lbslsat  33629  ply1degltdimlem  33635  lindsun  33638  ccfldextdgrr  33682  0ringirng  33689  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  algextdeglem6  33713  algextdeglem7  33714  algextdeglem8  33715  rtelextdg2lem  33717  constrsuc  33728  2sqr3minply  33738  lmatfvlem  33761  lmat22e11  33764  madjusmdetlem1  33773  zarmxt1  33826  sqsscirc1  33854  ordtrest2NEW  33869  lmlim  33893  qqh0  33930  qqh1  33931  qqhcn  33937  qqhucn  33938  rrhcn  33943  cnrrext  33956  rrhre  33967  brsigarn  34148  sxval  34154  measvuni  34178  measunl  34180  measinblem  34184  volmeas  34195  braew  34206  aean  34208  sxbrsigalem3  34237  sxbrsiga  34255  0elcarsg  34272  inelcarsg  34276  carsgclctunlem1  34282  carsgclctunlem2  34284  omsmeas  34288  sitgval  34297  sitgclg  34307  sitmcl  34316  eulerpart  34347  fiblem  34363  fibp1  34366  fib2  34367  fib3  34368  fib4  34369  fib5  34370  fib6  34371  probdif  34385  probfinmeasbALTV  34394  cndprobnul  34402  bayesth  34404  dstrvprob  34436  coinflipprob  34444  coinflippvt  34449  ballotlem1  34451  ballotlem2  34453  ballotlemfval0  34460  ballotlem4  34463  ballotlemi1  34467  ballotlemii  34468  ballotlemic  34471  ballotlem1c  34472  ballotlemgun  34489  ballotth  34502  ccatmulgnn0dir  34519  signstfveq0  34554  signsvtp  34560  signsvtn  34561  signsvfpn  34562  signsvfnn  34563  ftc2re  34575  hgt750lemd  34625  hgt750lem  34628  2cycld  35106  derang0  35137  subfac0  35145  subfac1  35146  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  kur14lem6  35179  kur14lem7  35180  cvmliftlem5  35257  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem9  35279  cvmliftphtlem  35285  satfv1  35331  fmla1  35355  satfv0fvfmla0  35381  sategoelfvb  35387  msubff1  35524  iexpire  35697  rdgprc0  35757  rankaltopb  35943  rankeq1o  36135  itgeq12i  36170  cbvitgvw2  36214  clsun  36294  bj-rdg0gALT  37037  istoprelowl  37326  finxp1o  37358  finxpreclem4  37360  lindsdom  37574  matunitlindflem1  37576  ptrecube  37580  poimirlem3  37583  poimirlem4  37584  poimirlem30  37610  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  voliunnfl  37624  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  dvasin  37664  dvacos  37665  dvreasin  37666  dvreacos  37667  areacirclem4  37671  fdc  37705  prdsbnd2  37755  ismtyres  37768  reheibor  37799  rngo1cl  37899  rngokerinj  37935  riotaclbgBAD  38910  pmapglb  39727  trlcocnv  40677  dicval2  41136  dicopelval2  41138  dicelval2N  41139  djhfval  41354  djhcom  41362  dihjatcclem1  41375  dihjatcclem2  41376  dihprrnlem1N  41381  dihprrnlem2  41382  djhlsmat  41384  dvh4dimlem  41400  dvh2dim  41402  dvh3dim3N  41406  lclkrlem2c  41466  lclkrlem2m  41476  lclkrlem2v  41485  lcfrlem2  41500  lcfrlem18  41517  lcfrlem21  41520  lcfrlem23  41522  mapdindp4  41680  mapdh6eN  41697  mapdh7dN  41707  mapdh8ab  41734  mapdh8ad  41736  mapdh8b  41737  mapdh8e  41741  hdmap1l6e  41771  hdmapfval  41784  hdmapip1  41873  lcmfunnnd  41969  lcm1un  41970  lcm2un  41971  lcm3un  41972  lcm4un  41973  lcm5un  41974  lcm6un  41975  lcm7un  41976  lcm8un  41977  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c5lem3  42094  aks6d1c7lem2  42138  aks5lem3a  42146  unitscyglem3  42154  unitscyglem4  42155  aks5lem7  42157  asin1half  42339  acos1half  42340  prjspnval2  42573  mapfzcons  42672  mzpresrename  42706  mzpcompact2lem  42707  diophren  42769  rabren3dioph  42771  monotoddzzfi  42899  jm2.23  42953  expdiophlem1  42978  dnnumch1  43001  aomclem6  43016  dfac21  43023  lnrfg  43076  mendsca  43146  mendvscafval  43147  cytpval  43163  arearect  43176  aleph1min  43519  resqrtvalex  43607  imsqrtvalex  43608  comptiunov2i  43668  trclfvdecomr  43690  ntrclscls00  44028  hashnzfz  44289  hashnzfz2  44290  dvradcnv2  44316  binomcxplemnotnn0  44325  rfcnpre3  44933  rfcnpre4  44934  fprodabs2  45516  mccl  45519  lptioo2cn  45566  lptioo1cn  45567  limclner  45572  limsupresuz  45624  limsupequzmpt2  45639  limsupequzmptf  45652  climlimsupcex  45690  liminfresre  45700  liminfvalxr  45704  liminfresuz  45705  liminfequzmpt2  45712  liminf0  45714  liminfpnfuz  45737  cosnegpi  45788  dvnmul  45864  iblempty  45886  iblsplit  45887  stoweidlem11  45932  stoweidlem14  45935  wallispilem3  45988  wallispilem4  45989  wallispi2lem2  45993  dirkerper  46017  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem62  46089  fourierdlem69  46096  fourierdlem73  46100  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem108  46135  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  fouriersw  46152  etransclem23  46178  rrxtopn0  46214  sge0tsms  46301  sge0splitmpt  46332  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0isum  46348  sge0xaddlem2  46355  sge0xadd  46356  meaunle  46385  psmeasure  46392  meaiunincf  46404  meaiuninc3  46406  meaiininclem  46407  meaiininc  46408  caragen0  46427  caragenuncllem  46433  omeiunltfirp  46440  ovnsubadd  46493  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem3  46518  hoidmvlelem5  46520  hoidmvle  46521  hspmbllem2  46548  ovnsplit  46569  ovnovollem3  46579  vonioolem2  46602  vonct  46614  smflimlem4  46695  smflimsuplem2  46742  smflimsuplem8  46748  smflimsup  46749  tworepnotupword  46805  iccpartigtl  47297  iccpartlt  47298  fmtnorec2  47417  fmtno5  47431  nnsum4primeseven  47674  opstrgric  47779  ushggricedg  47780  usgrexmpl1vtx  47838  usgrexmpl1edg  47839  usgrexmpl2vtx  47843  usgrexmpl2edg  47844  cznrnglem  47982  cznabel  47983  cznrng  47984  cznnring  47985  rhmsubcALTVlem3  48006  ply1mulgsum  48119  lineval  48123  lcoop  48140  lincfsuppcl  48142  lincvalsng  48145  lincvalpr  48147  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  linc1  48154  lincsum  48158  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  snlindsntor  48200  lincresunit3lem2  48209  lincresunit3  48210  zlmodzxzldeplem3  48231  ldepsnlinc  48237  blen1  48318  blen2  48319  itcoval0mpt  48400  ackval1  48415  ackval2  48416  ackval3  48417  ackval40  48427  ackval41a  48428  ackval42  48430  ackval50  48432  lines  48465  rrxsphere  48482  2sphere  48483  itscnhlinecirc02plem3  48518  inlinecirc02p  48521  icccldii  48598  iscnrm3rlem3  48622  mndtcco  48758  aacllem  48895