Theorem fvexi 6905

Description: The value of a class exists. Inference form of fvex 6904. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fvexi.1	⊢ 𝐴 = (𝐹‘𝐵)

Assertion

Ref	Expression
fvexi	⊢ 𝐴 ∈ V

Proof of Theorem fvexi

Step	Hyp	Ref	Expression
1		fvexi.1	. 2 ⊢ 𝐴 = (𝐹‘𝐵)
2		fvex 6904	. 2 ⊢ (𝐹‘𝐵) ∈ V
3	1, 2	eqeltri 2824	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1534   ∈ wcel 2099  Vcvv 3469  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-nul 5300

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-sn 4625  df-pr 4627  df-uni 4904  df-iota 6494  df-fv 6550

This theorem is referenced by:  mptfvmpt  7234  ovex  7447  mapfienlem1  9420  climle  15608  climsup  15640  iserabs  15785  isumshft  15809  explecnv  15835  prodfclim1  15863  ressbas  17206  ressbasOLD  17207  ressbas2  17209  ressid  17216  ressval3d  17218  ressval3dOLD  17219  topnid  17408  prdsplusg  17431  prdsmulr  17432  prdsvsca  17433  prdsip  17434  prdsle  17435  prdsds  17437  prdshom  17440  prdsco  17441  pwselbasb  17461  pwsvscafval  17467  pwssca  17469  pwssnf1o  17471  imassca  17492  imasvsca  17493  imasle  17496  xpsrnbas  17544  xpssca  17549  xpsvsca  17550  isacs2  17624  homffval  17661  comfffval  17669  oppchomfval  17685  oppchomfvalOLD  17686  oppccofval  17688  oppccatid  17692  monfval  17706  oppcmon  17712  sectffval  17724  invffval  17732  rescbas  17803  rescbasOLD  17804  reschom  17805  rescco  17807  resccoOLD  17808  fullsubc  17827  isfunc  17841  isfuncd  17842  idfu2nd  17854  idfu1st  17856  cofu1st  17860  cofu2nd  17862  fucco  17945  fucid  17954  invfuc  17957  initoval  17973  termoval  17974  homafval  18009  arwval  18023  coafval  18044  coapm  18051  setccatid  18064  catchomfval  18082  catccofval  18084  catccatid  18086  elestrchom  18109  estrccatid  18113  xpcbas  18160  xpchomfval  18161  xpccofval  18164  1stf1  18174  1stf2  18175  2ndf1  18177  2ndf2  18178  prf1  18182  prf2fval  18183  evlf2  18201  evlf1  18203  curf1fval  18207  curf11  18209  curf12  18210  curf1cl  18211  curf2  18212  curf2cl  18214  hof2fval  18238  yonedalem4a  18258  yonedalem4c  18260  yonedalem3  18263  yonedainv  18264  isdrs  18284  ispos  18297  odupos  18311  pltfval  18314  lubfval  18333  lubeldm  18336  lubval  18339  glbfval  18346  glbeldm  18349  glbval  18352  odulub  18390  odujoin  18391  oduglb  18392  odumeet  18393  clatlem  18485  clatlubcl2  18487  clatglbcl2  18489  isdlat  18505  ipolt  18518  ipopos  18519  isacs4lem  18527  plusffval  18597  issstrmgm  18604  gsumvalx  18627  gsumval  18628  ismgmhm  18647  issubmgm2  18654  submgmacs  18668  issubmnd  18712  ress0g  18713  ismhm  18733  0subm  18760  0mhm  18762  submacs  18770  pwsdiagmhm  18774  gsumz  18779  frmdplusg  18797  efmndplusg  18823  efmndmgm  18828  smndex1mgm  18850  grpinvfval  18926  grpsubfval  18931  grpsubfvalALT  18932  mulgfval  19016  mulgfvalALT  19017  mulgval  19018  issubg  19072  0subg  19097  0subgOLD  19098  subgacs  19107  nsgacs  19108  nmznsg  19114  eqgfval  19122  isghm  19161  gicen  19223  isga  19233  subgga  19242  orbstafun  19253  orbstaval  19254  orbsta  19255  cntzfval  19262  cntzval  19263  oppgplusfval  19290  symg2bas  19338  symgvalstruct  19342  symgvalstructOLD  19343  cayleylem2  19359  psgnfval  19446  odfval  19478  odinf  19509  dfod2  19510  0subgALT  19514  pgpfi1  19541  pgp0  19542  sylow1lem2  19545  sylow3lem6  19578  lsmfval  19584  lsmvalx  19585  oppglsm  19588  pj1fval  19640  efglem  19662  efgrelexlemb  19696  efgcpbllemb  19701  frgpeccl  19707  frgpmhm  19711  vrgpval  19713  frgpuplem  19718  frgpupf  19719  frgpupval  19720  frgpup1  19721  frgpup3lem  19723  frgpnabllem2  19820  iscygodd  19834  prmcyg  19840  lt6abl  19841  gsumval3a  19849  gsumval3  19853  gsumzres  19855  gsumzcl2  19856  gsumzf1o  19858  gsumreidx  19863  gsumzaddlem  19867  gsumzadd  19868  gsumzsplit  19873  gsummptshft  19882  gsumzmhm  19883  gsumzoppg  19890  gsumzinv  19891  gsummptfidminv  19893  gsumsub  19894  gsumpt  19908  gsummptf1o  19909  gsum2dlem1  19916  gsum2dlem2  19917  gsum2d  19918  gsum2d2lem  19919  gsumxp2  19926  fsfnn0gsumfsffz  19929  nn0gsumfz  19930  gsummptnn0fz  19932  dprdfid  19965  dprdfinv  19967  dprdfadd  19968  dprdfeq0  19970  dmdprdsplitlem  19985  dpjidcl  20006  ablfacrplem  20013  ablfacrp  20014  ablfacrp2  20015  ablfac1a  20017  ablfac1b  20018  ablfac1c  20019  ablfac1eu  20021  pgpfaclem2  20030  ablfaclem2  20034  ablfaclem3  20035  2nsgsimpgd  20050  prmgrpsimpgd  20062  ablsimpgprmd  20063  mgpplusg  20069  mgpress  20080  mgpressOLD  20081  issrg  20119  ring1ne0  20224  gsumdixp  20244  pwsmgp  20252  opprmulfval  20264  dvdsrval  20289  isunit  20301  unitgrp  20311  unitlinv  20321  unitrinv  20322  dvrfval  20330  rdivmuldivd  20341  rnghmval  20368  isrnghm  20369  c0snmgmhm  20390  c0snmhm  20391  isnzr2  20446  isnzr2hash  20447  0ring  20452  0ringdif  20453  01eq0ringOLD  20457  0ring01eqbi  20458  zrrnghm  20462  issubrg  20499  subrgugrp  20519  rngcrescrhm  20606  isdrng2  20627  drngmcl  20630  drngid2  20634  imadrhmcl  20674  subrgacs  20677  sdrgacs  20678  cntzsdrg  20679  subdrgint  20680  isabv  20688  staffval  20716  islmod  20736  scaffval  20752  lcomfsupp  20774  mptscmfsupp0  20799  rmodislmod  20802  rmodislmodOLD  20803  lssset  20806  islss  20807  lsssn0  20821  lssacs  20840  lspfval  20846  lspval  20848  lspcl  20849  lspuni0  20883  lss0v  20890  0lmhm  20914  lmhmvsca  20919  islbs  20950  islbs3  21032  lbsextlem1  21035  lbsextlem3  21037  lbsextlem4  21038  lbsext  21040  rnglidl0  21114  rsp1  21122  2idlval  21134  qusrhm  21159  rrgval  21223  rrgsupp  21227  expghm  21388  zrhrhmb  21423  zlmvsca  21438  zntoslem  21477  znfi  21480  znunithash  21485  psgnghm  21499  psgnghm2  21500  psgnevpmb  21506  ipffval  21567  ocvfval  21585  ocvval  21586  elocv  21587  thlbas  21615  thlbasOLD  21616  thlle  21617  thlleOLD  21618  thlleval  21619  thloc  21620  pjfval  21627  pjdm  21628  pjpm  21629  isobs  21641  frlmbas  21676  frlmbasf  21681  frlmvscafval  21687  frlmvscavalb  21691  frlmsslss2  21696  frlmip  21699  uvcvval  21707  uvcvvcl  21708  frlmssuvc2  21716  frlmsslsp  21717  ellspd  21723  elfilspd  21724  islinds2  21734  islindf4  21759  aspval  21793  psrbas  21865  psrelbas  21866  psrplusg  21868  psrmulr  21872  psrvscafval  21878  psrvscacl  21881  psr0lid  21883  psrlidm  21892  psrridm  21893  resspsradd  21905  resspsrmul  21906  resspsrvsca  21907  mvrval2  21912  mplsubglem  21928  mpllsslem  21929  mplsubrglem  21933  ressmpladd  21954  ressmplmul  21955  ressmplvsca  21956  mplmon  21960  mplmonmul  21961  mplcoe1  21962  opsrle  21972  opsrtoslem2  21987  mplmon2  21992  evlslem4  22007  psrbagev1  22008  psrbagev1OLD  22009  evlslem2  22012  evlslem3  22013  evlsval2  22020  selvval  22048  mhpval  22051  ismhp3  22054  psdfval  22069  coe1sfi  22119  coe1fsupp  22120  mptcoe1fsupp  22121  coe1ae0  22122  ressply1add  22135  ressply1mul  22136  ressply1vsca  22137  gsumply1subr  22139  psropprmul  22143  coe1tmmul2fv  22184  coe1pwmulfv  22186  ply1coe  22204  cply1coe0  22207  cply1coe0bi  22208  gsummoncoe1  22214  evls1fval  22225  evls1val  22226  evls1rhmlem  22227  evls1sca  22229  evls1gsumadd  22230  evls1gsummul  22231  evl1val  22235  evl1fval1lem  22236  fveval1fvcl  22239  evl1sca  22240  evl1var  22242  evl1addd  22247  evl1subd  22248  evl1muld  22249  evl1expd  22251  pf1f  22256  pf1mpf  22258  pf1ind  22261  evl1gsummul  22266  mamures  22279  mndvcl  22280  mamucl  22288  mamuvs1  22292  mamuvs2  22293  matbas2d  22312  matecl  22314  mamumat1cl  22328  mat1comp  22329  mamulid  22330  mamurid  22331  mat1ov  22337  matsc  22339  mat1dimelbas  22360  mat1dimmul  22365  mat1f1o  22367  dmatval  22381  dmatmulcl  22389  scmatval  22393  scmatscmiddistr  22397  mavmulcl  22436  1mavmul  22437  marrepfval  22449  marrepeval  22452  marepvfval  22454  submafval  22468  mdetfval  22475  mdetunilem9  22509  mdetuni0  22510  m2detleiblem3  22518  m2detleiblem4  22519  minmar1fval  22535  minmar1eval  22538  symgmatr01  22543  gsummatr01lem3  22546  gsummatr01  22548  smadiadetlem1a  22552  smadiadetlem3  22557  invrvald  22565  cpmat  22598  mat2pmatfval  22612  mat2pmatbas  22615  decpmatfsupp  22658  decpmatmulsumfsupp  22662  pmatcollpw3lem  22672  pmatcollpw3fi1lem2  22676  pm2mpval  22684  mply1topmatcl  22694  chmatval  22718  chpmatfval  22719  chfacffsupp  22745  chfacfscmul0  22747  chfacfscmulfsupp  22748  chfacfpmmul0  22751  chfacfpmmulfsupp  22752  cpmidpmatlem2  22760  cpmadumatpolylem1  22770  imastopn  23611  uzrest  23788  tmdgsum2  23987  distgp  23990  indistgp  23991  snclseqg  24007  tsmsval  24022  tsms0  24033  tsmsres  24035  tsmsxplem1  24044  tsmsxplem2  24045  ussid  24152  isusp  24153  ressust  24155  cnextucn  24195  prdsxmetlem  24261  nrmmetd  24470  nmfval  24484  tngds  24551  tngdsOLD  24552  tngnm  24555  tngngp2  24556  tngngpd  24557  tngngp  24558  tngngp3  24560  nmo0  24639  xrrest  24710  climcncf  24807  cphsubrglem  25092  cphcjcl  25098  tcphex  25132  ipcau2  25149  cmsss  25266  rrxip  25305  minveclem4a  25345  minveclem4  25347  mbflimsup  25582  mbflim  25584  mdegfval  25985  mdegleb  25987  mdegldg  25989  deg1val  26019  uc1pval  26062  mon1pval  26064  q1pval  26077  r1pval  26080  ply1remlem  26086  ply1rem  26087  fta1glem1  26089  fta1glem2  26090  fta1blem  26092  idomrootle  26094  ig1pval  26097  elqaalem3  26243  ulmcau  26318  ulmdvlem1  26323  ulmdvlem3  26325  mbfulm  26329  itgulm  26331  dchrplusg  27167  dchrmullid  27172  dchrinvcl  27173  dchrptlem2  27185  dchrptlem3  27186  dchrsum2  27188  sumdchr2  27190  dchr2sum  27193  axtgcont1  28259  tgjustc1  28266  tgjustc2  28267  tglowdim1  28291  tgldimor  28293  tgldim0eq  28294  iscgrgd  28304  isismt  28325  tglnfn  28338  tglnunirn  28339  tglngval  28342  legval  28375  ishlg  28393  hlcgrex  28407  hlcgreulem  28408  mirval  28446  midexlem  28483  israg  28488  perpln1  28501  perpln2  28502  isperp  28503  ishpg  28550  midf  28567  ismidb  28569  lmif  28576  islmib  28578  iscgra  28600  isinag  28629  isleag  28638  iseqlg  28658  ttgval  28666  ttgvalOLD  28667  ttgitvval  28679  setsvtx  28835  uhgrunop  28875  incistruhgr  28879  upgrunop  28919  umgrunop  28921  usgriedgleord  29028  uspgredgleord  29032  uhgr0vsize0  29039  lfuhgr1v0e  29054  uhgrspanop  29096  upgrspanop  29097  umgrspanop  29098  usgrspanop  29099  uhgrspan1lem1  29100  upgrres1lem1  29109  usgredgffibi  29124  fusgredgfi  29125  usgr1v0e  29126  nbgr2vtx1edg  29150  nbuhgr2vtx1edgb  29152  nbfusgrlevtxm1  29177  nbfusgrlevtxm2  29178  uvtx01vtx  29197  cplgr1vlem  29229  cplgr1v  29230  cusgrsize2inds  29254  cusgrfilem3  29258  sizusglecusg  29264  fusgrmaxsize  29265  vtxdgfval  29268  vtxdun  29282  vtxd0nedgb  29289  p1evtxdeqlem  29313  p1evtxdeq  29314  p1evtxdp1  29315  usgrvd0nedg  29334  vtxdginducedm1lem1  29340  vtxdginducedm1lem4  29343  vtxdginducedm1  29344  vtxdginducedm1fi  29345  finsumvtxdg2ssteplem4  29349  rusgrnumwrdl2  29387  wksfval  29410  iswlkg  29414  wlkonprop  29459  wlkp1lem3  29476  wlkp1lem8  29481  wlkp1  29482  wksonproplem  29505  wksonproplemOLD  29506  wwlks  29633  wwlksnon  29649  wspthsnon  29650  clwwlk  29780  0wlkonlem2  29916  conngrv2edg  29992  eupthp1  30013  eupth2eucrct  30014  eupthvdres  30032  eupth2lem3  30033  eupth2lemb  30034  3cyclfrgrrn  30083  frgrwopreglem1  30109  frgrwopreg1  30115  imsmetlem  30487  dipfval  30499  sspval  30520  islno  30550  nmooval  30560  nmounbseqi  30574  nmobndseqi  30576  0ofval  30584  0oval  30585  ajfval  30606  isph  30619  phpar  30621  ajval  30658  ubthlem1  30667  ubthlem2  30668  minvecolem4b  30675  minvecolem4  30677  minvecolem5  30678  hlex  30695  ressplusf  32666  ressnm  32667  oppglt  32671  ressprs  32672  oduprs  32673  ismnt  32692  mgcval  32696  gsummptres  32744  gsummptres2  32745  gsumpart  32747  gsumhashmul  32748  inftmrel  32866  isinftm  32867  gsumvsca1  32911  ress1r  32919  ringinvval  32920  dvrcan5  32921  rmfsupp2  32923  fldgenval  32939  ofldlt1  32968  resvsca  32981  quslmod  33010  islinds5  33019  ellspds  33020  elrsp  33025  linds2eq  33036  elringlsm  33042  lsmsnpridl  33047  grplsm0l  33052  qusima  33058  nsgmgc  33062  nsgqusf1o  33066  elrspunidl  33079  elrspunsn  33080  drngidlhash  33085  prmidl0  33102  oppreqg  33130  opprqusbas  33135  qsdrngi  33142  idlsrgbas  33151  idlsrgplusg  33152  idlsrgmulr  33154  idlsrgtset  33155  rprmval  33166  fply1  33169  evls1fvf  33173  evls1expd  33175  evls1fpws  33182  evls1addd  33184  evls1muld  33186  evls1vsca  33187  r1pquslmic  33213  resssra  33219  dimval  33230  dimvalfi  33231  lvecdim0  33236  ply1degltdimlem  33252  irngval  33295  elirng  33296  irngss  33297  irngnzply1lem  33300  minplyval  33312  mdetpmtr1  33360  rspectopn  33404  zarcls0  33405  zarcls  33411  zartopn  33412  zarmxt1  33417  rhmpreimacnlem  33421  rhmpreimacn  33422  pstmfval  33433  ordtrest2NEW  33460  ordtconnlem1  33461  fsumcvg4  33487  pl1cn  33492  qqhval  33511  sibf0  33890  sitgclg  33898  sitgaddlemb  33904  eulerpartlemgvv  33932  afsval  34239  pthhashvtx  34673  usgrcyclgt2v  34677  cusgr3cyclex  34682  acycgr2v  34696  cusgracyclt3v  34702  mrsubfval  35054  mrsubcv  35056  mrsubff  35058  mrsubrn  35059  elmrsubrn  35066  msubfval  35070  msubff  35076  mpstval  35081  elmpst  35082  msrval  35084  mstaval  35090  msubvrs  35106  mclsssvlem  35108  mclsval  35109  mclsind  35116  mppsval  35118  climlec3  35264  sdclem2  37150  sdclem1  37151  caures  37168  heiborlem3  37221  heibor  37229  grpokerinj  37301  rngoi  37307  dvrunz  37362  isdrngo1  37364  isdrngo2  37366  isrngohom  37373  idlval  37421  isidl  37422  0idl  37433  0rngo  37435  divrngidl  37436  smprngopr  37460  igenval  37469  lshpset  38387  lsatset  38399  lcvfbr  38429  islfl  38469  lfl0f  38478  lfl1  38479  lfladd0l  38483  lflnegl  38485  lflvscl  38486  lflvsdi1  38487  lflvsdi2  38488  lflvsdi2a  38489  lflvsass  38490  lfl0sc  38491  lflsc0N  38492  lfl1sc  38493  lkr0f  38503  lkrsc  38506  eqlkr2  38509  ldualvbase  38535  ldualfvadd  38537  ldualvaddval  38540  ldualsca  38541  ldualfvs  38545  ldualvsval  38547  isopos  38589  cmtfvalN  38619  cvrfval  38677  pats  38694  glbconNOLD  38787  llnset  38915  lplnset  38939  lvolset  38982  lineset  39148  isline  39149  pointsetN  39151  psubspset  39154  ispsubsp  39155  pmapval  39167  paddfval  39207  paddval  39208  pclfvalN  39299  pclvalN  39300  polfvalN  39314  polvalN  39315  psubclsetN  39346  ispsubclN  39347  watvalN  39403  lhpset  39405  lautset  39492  islaut  39493  pautsetN  39508  ispautN  39509  ldilset  39519  ltrnset  39528  dilsetN  39563  cdleme26e  39769  cdleme26eALTN  39771  cdleme26fALTN  39772  cdleme26f  39773  cdleme26f2ALTN  39774  cdleme26f2  39775  cdlemefs32sn1aw  39824  cdleme43fsv1snlem  39830  cdleme41sn3a  39843  cdleme32a  39851  cdleme40m  39877  cdleme40n  39878  cdleme42b  39888  tgrpbase  40156  tgrpopr  40157  istendo  40170  tendopl  40186  tendo02  40197  erngbase  40211  erngfplus  40212  erngfmul  40215  erngbase-rN  40219  erngfplus-rN  40220  erngfmul-rN  40223  cdlemk36  40323  cdlemkid  40346  dvasca  40416  dvavbase  40423  dvafvadd  40424  dvafvsca  40426  diafval  40441  diaval  40442  dvhsca  40492  dvhvbase  40497  dvhfvadd  40501  dvhfvsca  40510  docafvalN  40532  docavalN  40533  djafvalN  40544  djavalN  40545  dibfval  40551  dibopelvalN  40553  dibopelval2  40555  dibelval3  40557  diblsmopel  40581  dicfval  40585  dicval  40586  cdlemn11a  40617  dihvalcqpre  40645  dihopelvalcpre  40658  dihord6apre  40666  dihpN  40746  dochfval  40760  dochval  40761  djhfval  40807  djhval  40808  islpolN  40893  lpolconN  40897  dochpolN  40900  lcfrlem9  40960  lcd0vvalN  41023  mapdval  41038  mapd1o  41058  mapdunirnN  41060  mapdhval  41134  mapdhval0  41135  hvmapfval  41169  hvmapval  41170  hdmap1fval  41206  hdmap1vallem  41207  hgmapfval  41296  hlhilset  41344  hlhilbase  41346  hlhilplus  41347  hlhilvsca  41361  hlhilip  41362  hlhilnvl  41364  hlhillsm  41370  hlhillcs  41372  hashscontpow  41526  frlmfielbas  41660  frlm0vald  41691  evlsval3  41714  evlsbagval  41721  evlselv  41742  fsuppind  41745  fsuppssind  41748  mhpind  41749  mhphf  41752  islssfgi  42418  pwssplit4  42435  frlmpwfi  42444  mendplusgfval  42531  mendmulrfval  42533  mendvscafval  42536  idomodle  42541  deg1mhm  42551  mnringelbased  43574  mnring0g2d  43580  mnringmulrd  43581  mnringmulrcld  43588  dvgrat  43672  uzmptshftfval  43706  climexp  44916  climinf  44917  climneg  44921  climdivf  44923  climconstmpt  44969  climresmpt  44970  climsubmpt  44971  fnlimfvre  44985  limsupvaluz  45019  limsupequzmpt2  45029  climuzlem  45054  climisp  45057  climxrrelem  45060  climxrre  45061  limsupgtlem  45088  liminflelimsupuz  45096  liminfgelimsupuz  45099  liminfequzmpt2  45102  liminfvaluz  45103  limsupvaluz3  45109  climliminflimsupd  45112  liminfreuzlem  45113  liminfltlem  45115  liminflimsupclim  45118  liminflbuz2  45126  liminfpnfuz  45127  xlimclim2lem  45150  climxlim2  45157  sge0isum  45738  sge0uzfsumgt  45755  sge0seq  45757  meaiunlelem  45779  caragendifcl  45825  omeiunle  45828  omeiunltfirp  45830  carageniuncl  45834  caragensal  45836  opnssborel  45946  smflimlem6  46087  smfpimcc  46119  smflimmpt  46121  smflimsuplem4  46134  smflimsuplem6  46136  smflimsuplem8  46138  smfliminflem  46141  uspgrimprop  47094  isuspgrim  47096  gricen  47114  ushggricedg  47116  upwlksfval  47120  isupwlkg  47122  copisnmnd  47154  zlidlring  47219  cznrng  47246  cznnring  47247  rngchomfvalALTV  47252  rngccofvalALTV  47255  rngccatidALTV  47257  rngcrescrhmALTV  47265  ringchomfvalALTV  47286  ringccofvalALTV  47289  ringccatidALTV  47291  ofaddmndmap  47330  suppmptcfin  47366  mptcfsupp  47367  dmatALTbas  47392  lcoop  47402  linccl  47405  lcosn0  47411  lincvalsc0  47412  lcoc0  47413  linc0scn0  47414  linc1  47416  lincscmcl  47423  islinindfis  47440  lincext1  47445  lincext2  47446  lindslinindimp2lem2  47450  lindslinindimp2lem3  47451  lindsrng01  47459  snlindsntorlem  47461  snlindsntor  47462  ldepspr  47464  lincresunit1  47468  lincresunit2  47469  lines  47727  line  47728  rrxlines  47729  sphere  47743  rrxsphere  47744  functhinclem1  47970  thincciso  47978