Theorem fveq2i 6909

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 6906	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1536  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  fveq12i  6912  ot1stg  8026  ot2ndg  8027  ot3rdg  8028  wfrlem5OLD  8351  wfrlem14OLD  8360  tfr2a  8433  rdgsucmptf  8466  rdgsucmptnf  8467  rdg0n  8472  frsucmpt  8476  frsucmptn  8477  infiso  9545  inf3lemc  9663  cantnf  9730  wemapwe  9734  cnfcom2lem  9738  cnfcom2  9739  cnfcom3lem  9740  r1sucg  9806  rankprb  9888  rankopb  9889  ranksuc  9902  rankmapu  9915  cardiun  10019  alephsuc  10105  alephcard  10107  alephfplem2  10142  ackbij1lem8  10263  ackbij1lem13  10268  ackbij1lem14  10269  ackbij2lem2  10276  infpssrlem2  10341  fin23lem34  10383  fin23lem35  10384  aleph1  10608  pwcfsdom  10620  cfpwsdom  10621  alephom  10622  rankcf  10814  addpqnq  10975  mulpqnq  10978  addcomnq  10988  mulcomnq  10990  addclprlem2  11054  infrenegsup  12248  fseq1p1m1  13634  fldiv4p1lem1div2  13871  om2uzrdg  13993  uzrdgsuci  13997  fzennn  14005  axdc4uzlem  14020  seqp1d  14055  seqf1olem2  14079  facp1  14313  fac2  14314  fac3  14315  fac4  14316  4bc2eq6  14364  hashcard  14390  hasheq0  14398  hashun2  14418  hashun3  14419  hashprg  14430  hashprb  14432  hashprdifel  14433  hashp1i  14438  pr0hash2ex  14443  hashdif  14448  hashunlei  14460  hashfzo  14464  hashxplem  14468  hashfun  14472  hashimarn  14475  hashbclem  14487  hashbc  14488  hashf1lem2  14491  hashtpg  14520  ccatalpha  14627  s1len  14640  ccat2s1p2  14664  revs1  14799  cats1len  14895  lsws2  14939  lsws3  14940  lsws4  14941  rei  15191  imi  15192  sqrt1  15306  sqrt4  15307  sqrt9  15308  abs0  15320  absi  15321  sqreulem  15394  fsumabs  15833  fsumrelem  15839  o1fsum  15845  hashrabrex  15857  hashuni  15858  incexclem  15868  incexc  15869  isumnn0nn  15874  fprodefsum  16127  efsep  16142  sin0  16181  cos0  16182  ef01bndlem  16216  cos2bnd  16220  sin4lt0  16227  ruclem6  16267  aleph1re  16277  pwp1fsum  16424  m1bits  16473  sadcaddlem  16490  sadaddlem  16499  sadeq  16505  algrp1  16607  eucalg  16620  prmind2  16718  dfphi2  16807  phiprmpw  16809  phimullem  16812  pockthlem  16938  pockthg  16939  prmunb  16947  prmreclem4  16952  vdwap1  17010  vdwlem12  17025  prmo2  17073  prmo3  17074  prmgaplem7  17090  prmo4  17161  prmo5  17162  prmo6  17163  imasvsca  17566  mreexdomd  17693  isoval  17812  yonedalem21  18329  yonedalem22  18334  oduleval  18345  odubas  18347  odubasOLD  18348  joincomALT  18458  meetcomALT  18460  lubsn  18539  isacs5lem  18602  acsmapd  18611  efmnd1hash  18917  efmnd1bas  18918  efmnd2hash  18919  ressmulgnnd  19108  oppgplusfval  19378  setsplusg  19380  oppglemOLD  19381  symgbas  19403  symghash  19409  symgplusg  19414  symg1hash  19421  symg2hash  19423  symgtset  19431  symggen  19502  psgnsn  19552  psgnprfval1  19554  psgnprfval2  19555  odngen  19609  sylow1lem1  19630  efgs1b  19768  efgsfo  19771  efgredlemg  19774  efgredlemd  19776  frgpuplem  19804  gsumzmhm  19969  gsumzinv  19977  dprd2da  20076  dmdprdsplit2lem  20079  pgpfaclem1  20115  mgpplusg  20155  mgplemOLD  20156  ringidval  20200  opprmulfval  20352  opprlem  20355  opprlemOLD  20356  isrhm2d  20503  rhm1  20505  rhmopp  20525  cntzsubrng  20583  rhmsubclem3  20703  rhmsubclem4  20704  subdrgint  20820  rmodislmod  20944  rmodislmodOLD  20945  lspprid2  21013  lsmpr  21105  lsppr  21109  lspsntri  21113  lbspropd  21115  lspexchn2  21150  lspindp2l  21153  lspindp2  21154  lspsnat  21164  lsppratlem1  21166  lsppratlem3  21168  lsppratlem4  21169  lidlrsppropd  21271  zrhpsgnodpm  21627  psgnfix1  21633  psgnfix2  21634  psgndiflemB  21635  dsmmbas2  21774  dsmmelbas  21776  dsmmsubg  21780  frlmip  21815  islinds2  21850  lindsind2  21856  lindfmm  21864  islindf4  21875  assamulgscmlem2  21937  evlsval  22127  selvval  22156  psropprmul  22254  ply1sca2  22270  ply1mpl0  22273  ply1mpl1  22275  coe1fzgsumd  22323  ply1fermltlchr  22331  evls1var  22357  evl1gsumd  22376  evl1varpw  22380  evl1varpwval  22381  evl1scvarpw  22382  mat1bas  22470  mat0dim0  22488  mat0dimid  22489  mat0dimscm  22490  mat0dimcrng  22491  mat1rhmelval  22501  dmatval  22513  scmatval  22525  mat1scmat  22560  1mavmul  22569  marrepfval  22581  marepvfval  22586  ma1repvcl  22591  ma1repveval  22592  submafval  22600  mdetfval1  22611  mdetralt  22629  mdetunilem7  22639  m2detleiblem3  22650  m2detleiblem4  22651  madufval  22658  maducoeval2  22661  madugsum  22664  minmar1fval  22667  cramerimplem1  22704  cramer0  22711  pmatcoe1fsupp  22722  cpmat  22730  mat2pmatfval  22744  mat2pmatmul  22752  idmatidpmat  22758  m2cpminv0  22782  pmatcollpwfi  22803  pmatcollpw3fi1lem1  22807  pm2mpval  22816  chpmatval2  22854  cpmidpmat  22894  cayleyhamilton1  22913  sn0cld  23113  lpdifsn  23166  restcls  23204  restntr  23205  ordtrest2  23227  leordtval  23236  pttoponconst  23620  ptclsg  23638  xkoptsub  23677  xkofvcn  23707  tgqtop  23735  hmeocls  23791  hmeontr  23792  ptcmpfi  23836  ptcmplem1  24075  tmdgsum  24118  utop2nei  24274  cuspcvg  24325  iscusp2  24326  cnextucn  24327  comet  24541  nrmmetd  24602  isngp3  24626  ngpds  24632  tngnm  24687  cnmetdval  24806  qdensere2  24832  tgioo3  24840  cnmpopc  24968  cnheibor  25000  htpyco2  25024  phtpyco2  25035  pco0  25060  pi1xfrcnv  25103  cnrbas  25188  cncvs  25191  cnnm  25207  ipcau2  25281  cfilfcls  25321  cncmet  25369  reust  25428  rrxprds  25436  rrxsca  25443  ehleudis  25465  ehleudisval  25466  pjthlem1  25484  ovolunlem1a  25544  ovolfiniun  25549  ovoliunlem2  25551  ovoliunlem3  25552  ovoliun  25553  ovolicc1  25564  ismbl2  25575  unmbl  25585  volinun  25594  volfiniun  25595  voliunlem1  25598  voliunlem2  25599  ioorinv  25624  mbfimaopnlem  25703  itg2cnlem2  25811  itg2cn  25812  dfitg  25818  cbvitgv  25826  itg0  25829  iblre  25843  itgreval  25846  itgitg2  25856  iblconst  25867  itgconst  25868  itgcn  25894  limcflflem  25929  dvn1  25976  dvlipcn  26047  c1lip2  26051  dvcnvrelem2  26071  ply1divalg2  26192  ply1remlem  26218  dgr0  26316  elqaalem2  26376  dvradcnv  26478  pserdvlem2  26486  pserdv2  26488  abelthlem6  26494  abelthlem9  26498  sinhalfpilem  26519  cospi  26528  sincos4thpi  26569  sincos6thpi  26572  sincos3rdpi  26573  pige3ALT  26576  sinkpi  26578  eflog  26632  logfac  26657  logdmopn  26705  logtayl  26716  cxpcn3  26805  root1eq1  26812  cxpeq  26814  logbleb  26840  logblt  26841  sqrt2cxp2logb9e3  26856  ang180lem1  26866  ang180lem2  26867  ang180lem4  26869  lawcos  26873  1cubrlem  26898  asin1  26951  atan0  26965  atan1  26985  log2cnv  27001  birthdaylem2  27009  lgamgulmlem2  27087  gam1  27122  ftalem3  27132  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  ppi1  27221  ppi1i  27225  ppi2i  27226  cht2  27229  cht3  27230  ppiub  27262  chtub  27270  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsval2lem  27365  lgsqrlem1  27404  lgsqrlem4  27407  lgsquadlem2  27439  chebbnd1  27530  rplogsumlem1  27542  rplogsumlem2  27543  dchrisum0flb  27568  mulog2sumlem2  27593  pntpbnd1a  27643  pntlemf  27663  nosepne  27739  noinfbnd2lem1  27789  bday0s  27887  bday1s  27890  left0s  27945  right0s  27946  left1s  27947  right1s  27948  precsexlem1  28245  precsexlem2  28246  zseo  28420  cchhllem  28915  cchhllemOLD  28916  axlowdimlem17  28987  graop  29060  setsiedg  29067  vtxvalsnop  29072  iedgvalsnop  29073  usgrexmpllem  29291  uhgrspan1lem2  29332  uhgrspan1lem3  29333  upgrres1lem2  29342  upgrres1lem3  29343  structtocusgr  29477  cusgrsizeinds  29484  cusgrsize  29486  vtxdg0e  29506  uspgrloopvtx  29547  uspgrloopiedg  29549  uspgrloopedg  29550  umgr2v2evtx  29553  umgr2v2eiedg  29555  vtxdginducedm1lem1  29571  vtxdginducedm1  29575  vtxdginducedm1fi  29576  finsumvtxdg2ssteplem1  29577  finsumvtxdg2ssteplem2  29578  finsumvtxdg2ssteplem3  29579  finsumvtxdg2ssteplem4  29580  finsumvtxdg2sstep  29581  finsumvtxdg2size  29582  wlkres  29702  wlkp1lem2  29706  trlreslem  29731  clwlkcompbp  29814  crctcshlem2  29847  crctcshwlkn0  29850  2wlkdlem1  29954  2wlkdlem2  29955  2wlkdlem4  29957  2pthdlem1  29959  2wlkond  29966  2pthd  29969  umgr2adedgwlk  29974  clwwlknclwwlkdifnum  30008  clwwlkccatlem  30017  clwlkclwwlkfo  30037  clwlknf1oclwwlkn  30112  clwwlknon2num  30133  0wlkon  30148  0clwlk  30158  0cycl  30162  1pthdlem1  30163  1pthdlem2  30164  1wlkdlem1  30165  1wlkdlem4  30168  1pthond  30172  lp1cycl  30180  wlk2v2elem2  30184  wlk2v2e  30185  3wlkdlem1  30187  3wlkdlem2  30188  3wlkdlem4  30190  3pthdlem1  30192  3wlkond  30199  3pthd  30202  3cycld  30206  3cyclpd  30207  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2eucrct  30245  eupthvdres  30263  eupth2lem3  30264  eucrct2eupth  30273  konigsbergvtx  30274  konigsbergiedg  30275  konigsberg  30285  2clwwlk2  30376  numclwlk1lem1  30397  numclwlk1  30399  numclwwlkqhash  30403  frgrreg  30422  ex-co  30466  ex-ceil  30476  ex-fac  30479  ex-hash  30481  ex-sqrt  30482  ex-prmo  30487  0vfval  30634  nvvop  30637  vsfval  30661  cnnvg  30706  cnnvs  30708  cnnvnm  30709  imsdval  30714  ipidsq  30738  nmblolbii  30827  blocnilem  30832  ip0i  30853  ip1ilem  30854  ipasslem10  30867  siilem1  30879  cnbn  30897  h2hva  31002  h2hsm  31003  h2hnm  31004  axhfvadd-zf  31010  axhvcom-zf  31011  axhvass-zf  31012  axhv0cl-zf  31013  axhvaddid-zf  31014  axhfvmul-zf  31015  axhvmulid-zf  31016  axhvmulass-zf  31017  axhvdistr1-zf  31018  axhvdistr2-zf  31019  axhvmul0-zf  31020  axhfi-zf  31021  axhis1-zf  31022  axhis2-zf  31023  axhis3-zf  31024  axhis4-zf  31025  axhcompl-zf  31026  norm-iii-i  31167  normsubi  31169  norm3difi  31175  normpar2i  31184  hh0v  31196  hhssva  31285  hhsssm  31286  hhssnm  31287  hhshsslem1  31295  hhsscms  31306  choc1  31355  shjcom  31386  pjhthlem1  31419  pjoc2i  31466  shs0i  31477  chj0i  31483  chdmj1i  31509  chjassi  31514  spansn0  31569  spanpr  31608  qlaxr4i  31662  pjadjii  31702  pjaddii  31703  pjmulii  31705  pjsubii  31706  pjcji  31712  pjnormi  31749  pjpythi  31750  ho0val  31778  lnop0  31994  lnophmlem2  32045  nmbdoplbi  32052  nmcopexi  32055  lnfn0i  32070  nmcfnexi  32079  nmopadji  32118  nmoptri2i  32127  nmopcoadj2i  32130  unierri  32132  branmfn  32133  pjbdlni  32177  pjclem2  32224  sto1i  32264  stm1ri  32272  st0  32277  hstrlem3a  32288  hstrlem4  32290  golem1  32299  superpos  32382  shatomistici  32389  iuninc  32580  hashunif  32815  pfxlsw2ccat  32919  chnub  32985  pmtrprfv2  33090  psgnfzto1st  33107  cyc2fv1  33123  cycpmco2lem4  33131  cycpmco2lem7  33134  cycpmco2  33135  cyc3fv1  33139  cyc3fv2  33140  cycpmrn  33145  cyc3genpmlem  33153  rlocval  33245  primefldchr  33282  xrge0slmod  33355  imaslmhm  33364  zringfrac  33561  evl1deg2  33581  evl1deg3  33582  lmimdim  33630  rlmdim  33636  rgmoddimOLD  33637  lbslsat  33643  ply1degltdimlem  33649  lindsun  33652  ccfldextdgrr  33696  0ringirng  33703  algextdeglem2  33723  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  algextdeglem6  33727  algextdeglem7  33728  algextdeglem8  33729  rtelextdg2lem  33731  constrsuc  33742  2sqr3minply  33752  lmatfvlem  33775  lmat22e11  33778  madjusmdetlem1  33787  zarmxt1  33840  sqsscirc1  33868  ordtrest2NEW  33883  lmlim  33907  qqh0  33946  qqh1  33947  qqhcn  33953  qqhucn  33954  rrhcn  33959  cnrrext  33972  rrhre  33983  brsigarn  34164  sxval  34170  measvuni  34194  measunl  34196  measinblem  34200  volmeas  34211  braew  34222  aean  34224  sxbrsigalem3  34253  sxbrsiga  34271  0elcarsg  34288  inelcarsg  34292  carsgclctunlem1  34298  carsgclctunlem2  34300  omsmeas  34304  sitgval  34313  sitgclg  34323  sitmcl  34332  eulerpart  34363  fiblem  34379  fibp1  34382  fib2  34383  fib3  34384  fib4  34385  fib5  34386  fib6  34387  probdif  34401  probfinmeasbALTV  34410  cndprobnul  34418  bayesth  34420  dstrvprob  34452  coinflipprob  34460  coinflippvt  34465  ballotlem1  34467  ballotlem2  34469  ballotlemfval0  34476  ballotlem4  34479  ballotlemi1  34483  ballotlemii  34484  ballotlemic  34487  ballotlem1c  34488  ballotlemgun  34505  ballotth  34518  ccatmulgnn0dir  34535  signstfveq0  34570  signsvtp  34576  signsvtn  34577  signsvfpn  34578  signsvfnn  34579  ftc2re  34591  hgt750lemd  34641  hgt750lem  34644  2cycld  35122  derang0  35153  subfac0  35161  subfac1  35162  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  kur14lem6  35195  kur14lem7  35196  cvmliftlem5  35273  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem9  35295  cvmliftphtlem  35301  satfv1  35347  fmla1  35371  satfv0fvfmla0  35397  sategoelfvb  35403  msubff1  35540  iexpire  35714  rdgprc0  35774  rankaltopb  35960  rankeq1o  36152  itgeq12i  36187  cbvitgvw2  36230  clsun  36310  bj-rdg0gALT  37053  istoprelowl  37342  finxp1o  37374  finxpreclem4  37376  lindsdom  37600  matunitlindflem1  37602  ptrecube  37606  poimirlem3  37609  poimirlem4  37610  poimirlem30  37636  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  voliunnfl  37650  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  dvasin  37690  dvacos  37691  dvreasin  37692  dvreacos  37693  areacirclem4  37697  fdc  37731  prdsbnd2  37781  ismtyres  37794  reheibor  37825  rngo1cl  37925  rngokerinj  37961  riotaclbgBAD  38935  pmapglb  39752  trlcocnv  40702  dicval2  41161  dicopelval2  41163  dicelval2N  41164  djhfval  41379  djhcom  41387  dihjatcclem1  41400  dihjatcclem2  41401  dihprrnlem1N  41406  dihprrnlem2  41407  djhlsmat  41409  dvh4dimlem  41425  dvh2dim  41427  dvh3dim3N  41431  lclkrlem2c  41491  lclkrlem2m  41501  lclkrlem2v  41510  lcfrlem2  41525  lcfrlem18  41542  lcfrlem21  41545  lcfrlem23  41547  mapdindp4  41705  mapdh6eN  41722  mapdh7dN  41732  mapdh8ab  41759  mapdh8ad  41761  mapdh8b  41762  mapdh8e  41766  hdmap1l6e  41796  hdmapfval  41809  hdmapip1  41898  lcmfunnnd  41993  lcm1un  41994  lcm2un  41995  lcm3un  41996  lcm4un  41997  lcm5un  41998  lcm6un  41999  lcm7un  42000  lcm8un  42001  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c5lem3  42118  aks6d1c7lem2  42162  aks5lem3a  42170  unitscyglem3  42178  unitscyglem4  42179  aks5lem7  42181  asin1half  42365  acos1half  42366  prjspnval2  42604  mapfzcons  42703  mzpresrename  42737  mzpcompact2lem  42738  diophren  42800  rabren3dioph  42802  monotoddzzfi  42930  jm2.23  42984  expdiophlem1  43009  dnnumch1  43032  aomclem6  43047  dfac21  43054  lnrfg  43107  mendsca  43173  mendvscafval  43174  cytpval  43190  arearect  43203  aleph1min  43546  resqrtvalex  43634  imsqrtvalex  43635  comptiunov2i  43695  trclfvdecomr  43717  ntrclscls00  44055  hashnzfz  44315  hashnzfz2  44316  dvradcnv2  44342  binomcxplemnotnn0  44351  rfcnpre3  44970  rfcnpre4  44971  fprodabs2  45550  mccl  45553  lptioo2cn  45600  lptioo1cn  45601  limclner  45606  limsupresuz  45658  limsupequzmpt2  45673  limsupequzmptf  45686  climlimsupcex  45724  liminfresre  45734  liminfvalxr  45738  liminfresuz  45739  liminfequzmpt2  45746  liminf0  45748  liminfpnfuz  45771  cosnegpi  45822  dvnmul  45898  iblempty  45920  iblsplit  45921  stoweidlem11  45966  stoweidlem14  45969  wallispilem3  46022  wallispilem4  46023  wallispi2lem2  46027  dirkerper  46051  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem62  46123  fourierdlem69  46130  fourierdlem73  46134  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem93  46154  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem100  46161  fourierdlem103  46164  fourierdlem104  46165  fourierdlem108  46169  fourierdlem110  46171  fourierdlem112  46173  fourierdlem113  46174  fouriersw  46186  etransclem23  46212  rrxtopn0  46248  sge0tsms  46335  sge0splitmpt  46366  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0isum  46382  sge0xaddlem2  46389  sge0xadd  46390  meaunle  46419  psmeasure  46426  meaiunincf  46438  meaiuninc3  46440  meaiininclem  46441  meaiininc  46442  caragen0  46461  caragenuncllem  46467  omeiunltfirp  46474  ovnsubadd  46527  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem3  46552  hoidmvlelem5  46554  hoidmvle  46555  hspmbllem2  46582  ovnsplit  46603  ovnovollem3  46613  vonioolem2  46636  vonct  46648  smflimlem4  46729  smflimsuplem2  46776  smflimsuplem8  46782  smflimsup  46783  tworepnotupword  46839  iccpartigtl  47347  iccpartlt  47348  fmtnorec2  47467  fmtno5  47481  nnsum4primeseven  47724  isubgredgss  47788  isubgredg  47789  opstrgric  47832  ushggricedg  47833  stgrvtx0  47864  stgrorder  47865  stgrnbgr0  47866  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  isubgr3stgrlem8  47875  isubgr3stgr  47877  usgrexmpl1vtx  47917  usgrexmpl1edg  47918  usgrexmpl2vtx  47922  usgrexmpl2edg  47923  gpgvtxel  47940  gpgedgel  47942  gpgvtx0  47943  gpgvtx1  47944  2ltceilhalf  47949  cznrnglem  48102  cznabel  48103  cznrng  48104  cznnring  48105  rhmsubcALTVlem3  48126  ply1mulgsum  48235  lineval  48239  lcoop  48256  lincfsuppcl  48258  lincvalsng  48261  lincvalpr  48263  lincvalsc0  48266  linc0scn0  48268  lincdifsn  48269  linc1  48270  lincsum  48274  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  snlindsntor  48316  lincresunit3lem2  48325  lincresunit3  48326  zlmodzxzldeplem3  48347  ldepsnlinc  48353  blen1  48433  blen2  48434  itcoval0mpt  48515  ackval1  48530  ackval2  48531  ackval3  48532  ackval40  48542  ackval41a  48543  ackval42  48545  ackval50  48547  lines  48580  rrxsphere  48597  2sphere  48598  itscnhlinecirc02plem3  48633  inlinecirc02p  48636  icccldii  48714  iscnrm3rlem3  48738  mndtcco  48893  aacllem  49031