Theorem fvexi 6906

Description: The value of a class exists. Inference form of fvex 6905. (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 6905	. 2 ⊢ (𝐹‘𝐵) ∈ V
3	1, 2	eqeltri 2830	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-fv 6552

This theorem is referenced by:  mptfvmpt  7230  ovex  7442  mapfienlem1  9400  climle  15584  climsup  15616  iserabs  15761  isumshft  15785  explecnv  15811  prodfclim1  15839  ressbas  17179  ressbasOLD  17180  ressbas2  17182  ressid  17189  ressval3d  17191  ressval3dOLD  17192  topnid  17381  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdsip  17407  prdsle  17408  prdsds  17410  prdshom  17413  prdsco  17414  pwselbasb  17434  pwsvscafval  17440  pwssca  17442  pwssnf1o  17444  imassca  17465  imasvsca  17466  imasle  17469  xpsrnbas  17517  xpssca  17522  xpsvsca  17523  isacs2  17597  homffval  17634  comfffval  17642  oppchomfval  17658  oppchomfvalOLD  17659  oppccofval  17661  oppccatid  17665  monfval  17679  oppcmon  17685  sectffval  17697  invffval  17705  rescbas  17776  rescbasOLD  17777  reschom  17778  rescco  17780  resccoOLD  17781  fullsubc  17800  isfunc  17814  isfuncd  17815  idfu2nd  17827  idfu1st  17829  cofu1st  17833  cofu2nd  17835  fucco  17915  fucid  17924  invfuc  17927  initoval  17943  termoval  17944  homafval  17979  arwval  17993  coafval  18014  coapm  18021  setccatid  18034  catchomfval  18052  catccofval  18054  catccatid  18056  elestrchom  18079  estrccatid  18083  xpcbas  18130  xpchomfval  18131  xpccofval  18134  1stf1  18144  1stf2  18145  2ndf1  18147  2ndf2  18148  prf1  18152  prf2fval  18153  evlf2  18171  evlf1  18173  curf1fval  18177  curf11  18179  curf12  18180  curf1cl  18181  curf2  18182  curf2cl  18184  hof2fval  18208  yonedalem4a  18228  yonedalem4c  18230  yonedalem3  18233  yonedainv  18234  isdrs  18254  ispos  18267  odupos  18281  pltfval  18284  lubfval  18303  lubeldm  18306  lubval  18309  glbfval  18316  glbeldm  18319  glbval  18322  odulub  18360  odujoin  18361  oduglb  18362  odumeet  18363  clatlem  18455  clatlubcl2  18457  clatglbcl2  18459  isdlat  18475  ipolt  18488  ipopos  18489  isacs4lem  18497  plusffval  18567  issstrmgm  18572  gsumvalx  18595  gsumval  18596  issubmnd  18652  ress0g  18653  ismhm  18673  0subm  18698  0mhm  18700  submacs  18708  pwsdiagmhm  18712  gsumz  18717  frmdplusg  18735  efmndplusg  18761  efmndmgm  18766  smndex1mgm  18788  grpinvfval  18863  grpsubfval  18868  grpsubfvalALT  18869  mulgfval  18952  mulgfvalALT  18953  mulgval  18954  issubg  19006  0subg  19031  0subgOLD  19032  subgacs  19041  nsgacs  19042  nmznsg  19048  eqgfval  19056  isghm  19092  gicen  19151  isga  19155  subgga  19164  orbstafun  19175  orbstaval  19176  orbsta  19177  cntzfval  19184  cntzval  19185  oppgplusfval  19212  symg2bas  19260  symgvalstruct  19264  symgvalstructOLD  19265  cayleylem2  19281  psgnfval  19368  odfval  19400  odinf  19431  dfod2  19432  0subgALT  19436  pgpfi1  19463  pgp0  19464  sylow1lem2  19467  sylow3lem6  19500  lsmfval  19506  lsmvalx  19507  oppglsm  19510  pj1fval  19562  efglem  19584  efgrelexlemb  19618  efgcpbllemb  19623  frgpeccl  19629  frgpmhm  19633  vrgpval  19635  frgpuplem  19640  frgpupf  19641  frgpupval  19642  frgpup1  19643  frgpup3lem  19645  frgpnabllem2  19742  iscygodd  19756  prmcyg  19762  lt6abl  19763  gsumval3a  19771  gsumval3  19775  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumreidx  19785  gsumzaddlem  19789  gsumzadd  19790  gsumzsplit  19795  gsummptshft  19804  gsumzmhm  19805  gsumzoppg  19812  gsumzinv  19813  gsummptfidminv  19815  gsumsub  19816  gsumpt  19830  gsummptf1o  19831  gsum2dlem1  19838  gsum2dlem2  19839  gsum2d  19840  gsum2d2lem  19841  gsumxp2  19848  fsfnn0gsumfsffz  19851  nn0gsumfz  19852  gsummptnn0fz  19854  dprdfid  19887  dprdfinv  19889  dprdfadd  19890  dprdfeq0  19892  dmdprdsplitlem  19907  dpjidcl  19928  ablfacrplem  19935  ablfacrp  19936  ablfacrp2  19937  ablfac1a  19939  ablfac1b  19940  ablfac1c  19941  ablfac1eu  19943  pgpfaclem2  19952  ablfaclem2  19956  ablfaclem3  19957  2nsgsimpgd  19972  prmgrpsimpgd  19984  ablsimpgprmd  19985  mgpplusg  19991  mgpress  20002  mgpressOLD  20003  issrg  20011  ring1ne0  20111  gsumdixp  20131  pwsmgp  20140  opprmulfval  20152  dvdsrval  20175  isunit  20187  unitgrp  20197  unitlinv  20207  unitrinv  20208  dvrfval  20216  rdivmuldivd  20227  isnzr2  20297  isnzr2hash  20298  0ring  20303  01eq0ringOLD  20306  0ring01eqbi  20307  issubrg  20319  subrgugrp  20338  isdrng2  20371  drngmcl  20374  drngid2  20378  imadrhmcl  20413  subrgacs  20416  sdrgacs  20417  cntzsdrg  20418  subdrgint  20419  isabv  20427  staffval  20455  islmod  20475  scaffval  20490  lcomfsupp  20512  mptscmfsupp0  20537  rmodislmod  20540  rmodislmodOLD  20541  lssset  20544  islss  20545  lsssn0  20558  lssacs  20578  lspfval  20584  lspval  20586  lspcl  20587  lspuni0  20621  lss0v  20627  0lmhm  20651  lmhmvsca  20656  islbs  20687  islbs3  20768  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  lbsext  20776  rsp1  20849  2idlval  20858  qusrhm  20874  rrgval  20903  rrgsupp  20907  expghm  21045  zrhrhmb  21060  zlmvsca  21075  zntoslem  21112  znfi  21115  znunithash  21120  psgnghm  21133  psgnghm2  21134  psgnevpmb  21140  ipffval  21201  ocvfval  21219  ocvval  21220  elocv  21221  thlbas  21249  thlbasOLD  21250  thlle  21251  thlleOLD  21252  thlleval  21253  thloc  21254  pjfval  21261  pjdm  21262  pjpm  21263  isobs  21275  frlmbas  21310  frlmbasf  21315  frlmvscafval  21321  frlmvscavalb  21325  frlmsslss2  21330  frlmip  21333  uvcvval  21341  uvcvvcl  21342  frlmssuvc2  21350  frlmsslsp  21351  ellspd  21357  elfilspd  21358  islinds2  21368  islindf4  21393  aspval  21427  psrbas  21497  psrelbas  21498  psrplusg  21500  psrmulr  21503  psrvscafval  21509  psrvscacl  21512  psr0lid  21514  psrlidm  21523  psrridm  21524  resspsradd  21536  resspsrmul  21537  resspsrvsca  21538  mvrval2  21542  mplsubglem  21558  mpllsslem  21559  mplsubrglem  21563  ressmpladd  21584  ressmplmul  21585  ressmplvsca  21586  mplmon  21590  mplmonmul  21591  mplcoe1  21592  opsrle  21602  opsrtoslem2  21617  mplmon2  21622  evlslem4  21637  psrbagev1  21638  psrbagev1OLD  21639  evlslem2  21642  evlslem3  21643  evlsval2  21650  selvval  21681  mhpval  21683  ismhp3  21686  coe1sfi  21737  coe1fsupp  21738  mptcoe1fsupp  21739  coe1ae0  21740  ressply1add  21752  ressply1mul  21753  ressply1vsca  21754  gsumply1subr  21756  psropprmul  21760  coe1tmmul2fv  21800  coe1pwmulfv  21802  ply1coe  21820  cply1coe0  21823  cply1coe0bi  21824  gsummoncoe1  21828  evls1fval  21838  evls1val  21839  evls1rhmlem  21840  evls1sca  21842  evls1gsumadd  21843  evls1gsummul  21844  evl1val  21848  evl1fval1lem  21849  fveval1fvcl  21852  evl1sca  21853  evl1var  21855  evl1addd  21860  evl1subd  21861  evl1muld  21862  evl1expd  21864  pf1f  21869  pf1mpf  21871  pf1ind  21874  evl1gsummul  21879  mamures  21892  mndvcl  21893  mamucl  21901  mamuvs1  21905  mamuvs2  21906  matbas2d  21925  matecl  21927  mamumat1cl  21941  mat1comp  21942  mamulid  21943  mamurid  21944  mat1ov  21950  matsc  21952  mat1dimelbas  21973  mat1dimmul  21978  mat1f1o  21980  dmatval  21994  dmatmulcl  22002  scmatval  22006  scmatscmiddistr  22010  mavmulcl  22049  1mavmul  22050  marrepfval  22062  marrepeval  22065  marepvfval  22067  submafval  22081  mdetfval  22088  mdetunilem9  22122  mdetuni0  22123  m2detleiblem3  22131  m2detleiblem4  22132  minmar1fval  22148  minmar1eval  22151  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01  22161  smadiadetlem1a  22165  smadiadetlem3  22170  invrvald  22178  cpmat  22211  mat2pmatfval  22225  mat2pmatbas  22228  decpmatfsupp  22271  decpmatmulsumfsupp  22275  pmatcollpw3lem  22285  pmatcollpw3fi1lem2  22289  pm2mpval  22297  mply1topmatcl  22307  chmatval  22331  chpmatfval  22332  chfacffsupp  22358  chfacfscmul0  22360  chfacfscmulfsupp  22361  chfacfpmmul0  22364  chfacfpmmulfsupp  22365  cpmidpmatlem2  22373  cpmadumatpolylem1  22383  imastopn  23224  uzrest  23401  tmdgsum2  23600  distgp  23603  indistgp  23604  snclseqg  23620  tsmsval  23635  tsms0  23646  tsmsres  23648  tsmsxplem1  23657  tsmsxplem2  23658  ussid  23765  isusp  23766  ressust  23768  cnextucn  23808  prdsxmetlem  23874  nrmmetd  24083  nmfval  24097  tngds  24164  tngdsOLD  24165  tngnm  24168  tngngp2  24169  tngngpd  24170  tngngp  24171  tngngp3  24173  nmo0  24252  xrrest  24323  climcncf  24416  cphsubrglem  24694  cphcjcl  24700  tcphex  24734  ipcau2  24751  cmsss  24868  rrxip  24907  minveclem4a  24947  minveclem4  24949  mbflimsup  25183  mbflim  25185  mdegfval  25580  mdegleb  25582  mdegldg  25584  deg1val  25614  uc1pval  25657  mon1pval  25659  q1pval  25671  r1pval  25674  ply1remlem  25680  ply1rem  25681  fta1glem1  25683  fta1glem2  25684  fta1blem  25686  ig1pval  25690  elqaalem3  25834  ulmcau  25907  ulmdvlem1  25912  ulmdvlem3  25914  mbfulm  25918  itgulm  25920  dchrplusg  26750  dchrmullid  26755  dchrinvcl  26756  dchrptlem2  26768  dchrptlem3  26769  dchrsum2  26771  sumdchr2  26773  dchr2sum  26776  axtgcont1  27719  tgjustc1  27726  tgjustc2  27727  tglowdim1  27751  tgldimor  27753  tgldim0eq  27754  iscgrgd  27764  isismt  27785  tglnfn  27798  tglnunirn  27799  tglngval  27802  legval  27835  ishlg  27853  hlcgrex  27867  hlcgreulem  27868  mirval  27906  midexlem  27943  israg  27948  perpln1  27961  perpln2  27962  isperp  27963  ishpg  28010  midf  28027  ismidb  28029  lmif  28036  islmib  28038  iscgra  28060  isinag  28089  isleag  28098  iseqlg  28118  ttgval  28126  ttgvalOLD  28127  ttgitvval  28139  setsvtx  28295  uhgrunop  28335  incistruhgr  28339  upgrunop  28379  umgrunop  28381  usgriedgleord  28485  uspgredgleord  28489  uhgr0vsize0  28496  lfuhgr1v0e  28511  uhgrspanop  28553  upgrspanop  28554  umgrspanop  28555  usgrspanop  28556  uhgrspan1lem1  28557  upgrres1lem1  28566  usgredgffibi  28581  fusgredgfi  28582  usgr1v0e  28583  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  nbfusgrlevtxm1  28634  nbfusgrlevtxm2  28635  uvtx01vtx  28654  cplgr1vlem  28686  cplgr1v  28687  cusgrsize2inds  28710  cusgrfilem3  28714  sizusglecusg  28720  fusgrmaxsize  28721  vtxdgfval  28724  vtxdun  28738  vtxd0nedgb  28745  p1evtxdeqlem  28769  p1evtxdeq  28770  p1evtxdp1  28771  usgrvd0nedg  28790  vtxdginducedm1lem1  28796  vtxdginducedm1lem4  28799  vtxdginducedm1  28800  vtxdginducedm1fi  28801  finsumvtxdg2ssteplem4  28805  rusgrnumwrdl2  28843  wksfval  28866  iswlkg  28870  wlkonprop  28915  wlkp1lem3  28932  wlkp1lem8  28937  wlkp1  28938  wksonproplem  28961  wksonproplemOLD  28962  wwlks  29089  wwlksnon  29105  wspthsnon  29106  clwwlk  29236  0wlkonlem2  29372  conngrv2edg  29448  eupthp1  29469  eupth2eucrct  29470  eupthvdres  29488  eupth2lem3  29489  eupth2lemb  29490  3cyclfrgrrn  29539  frgrwopreglem1  29565  frgrwopreg1  29571  imsmetlem  29943  dipfval  29955  sspval  29976  islno  30006  nmooval  30016  nmounbseqi  30030  nmobndseqi  30032  0ofval  30040  0oval  30041  ajfval  30062  isph  30075  phpar  30077  ajval  30114  ubthlem1  30123  ubthlem2  30124  minvecolem4b  30131  minvecolem4  30133  minvecolem5  30134  hlex  30151  ressplusf  32127  ressnm  32128  oppglt  32132  ressprs  32133  oduprs  32134  ismnt  32153  mgcval  32157  gsummptres  32204  gsummptres2  32205  gsumpart  32207  gsumhashmul  32208  inftmrel  32326  isinftm  32327  gsumvsca1  32371  ress1r  32383  ringinvval  32384  dvrcan5  32385  rmfsupp2  32387  fldgenval  32402  ofldlt1  32431  resvsca  32444  quslmod  32469  islinds5  32480  ellspds  32481  elrsp  32486  linds2eq  32497  elringlsm  32503  lsmsnpridl  32508  grplsm0l  32513  qusima  32519  nsgmgc  32523  nsgqusf1o  32527  elrspunidl  32546  elrspunsn  32547  drngidlhash  32552  prmidl0  32569  oppreqg  32597  opprqusbas  32602  qsdrngi  32609  idlsrgbas  32618  idlsrgplusg  32619  idlsrgmulr  32621  idlsrgtset  32622  rprmval  32633  fply1  32637  evls1fvf  32642  evls1expd  32644  evls1fpws  32646  evls1addd  32648  evls1muld  32649  evls1vsca  32650  dimval  32686  dimvalfi  32687  lvecdim0  32691  ply1degltdimlem  32707  irngval  32749  elirng  32750  irngss  32751  irngnzply1lem  32754  minplyval  32766  mdetpmtr1  32803  rspectopn  32847  zarcls0  32848  zarcls  32854  zartopn  32855  zarmxt1  32860  rhmpreimacnlem  32864  rhmpreimacn  32865  pstmfval  32876  ordtrest2NEW  32903  ordtconnlem1  32904  fsumcvg4  32930  pl1cn  32935  qqhval  32954  sibf0  33333  sitgclg  33341  sitgaddlemb  33347  eulerpartlemgvv  33375  afsval  33683  pthhashvtx  34118  usgrcyclgt2v  34122  cusgr3cyclex  34127  acycgr2v  34141  cusgracyclt3v  34147  mrsubfval  34499  mrsubcv  34501  mrsubff  34503  mrsubrn  34504  elmrsubrn  34511  msubfval  34515  msubff  34521  mpstval  34526  elmpst  34527  msrval  34529  mstaval  34535  msubvrs  34551  mclsssvlem  34553  mclsval  34554  mclsind  34561  mppsval  34563  climlec3  34703  sdclem2  36610  sdclem1  36611  caures  36628  heiborlem3  36681  heibor  36689  grpokerinj  36761  rngoi  36767  dvrunz  36822  isdrngo1  36824  isdrngo2  36826  isrngohom  36833  idlval  36881  isidl  36882  0idl  36893  0rngo  36895  divrngidl  36896  smprngopr  36920  igenval  36929  lshpset  37848  lsatset  37860  lcvfbr  37890  islfl  37930  lfl0f  37939  lfl1  37940  lfladd0l  37944  lflnegl  37946  lflvscl  37947  lflvsdi1  37948  lflvsdi2  37949  lflvsdi2a  37950  lflvsass  37951  lfl0sc  37952  lflsc0N  37953  lfl1sc  37954  lkr0f  37964  lkrsc  37967  eqlkr2  37970  ldualvbase  37996  ldualfvadd  37998  ldualvaddval  38001  ldualsca  38002  ldualfvs  38006  ldualvsval  38008  isopos  38050  cmtfvalN  38080  cvrfval  38138  pats  38155  glbconNOLD  38248  llnset  38376  lplnset  38400  lvolset  38443  lineset  38609  isline  38610  pointsetN  38612  psubspset  38615  ispsubsp  38616  pmapval  38628  paddfval  38668  paddval  38669  pclfvalN  38760  pclvalN  38761  polfvalN  38775  polvalN  38776  psubclsetN  38807  ispsubclN  38808  watvalN  38864  lhpset  38866  lautset  38953  islaut  38954  pautsetN  38969  ispautN  38970  ldilset  38980  ltrnset  38989  dilsetN  39024  cdleme26e  39230  cdleme26eALTN  39232  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme41sn3a  39304  cdleme32a  39312  cdleme40m  39338  cdleme40n  39339  cdleme42b  39349  tgrpbase  39617  tgrpopr  39618  istendo  39631  tendopl  39647  tendo02  39658  erngbase  39672  erngfplus  39673  erngfmul  39676  erngbase-rN  39680  erngfplus-rN  39681  erngfmul-rN  39684  cdlemk36  39784  cdlemkid  39807  dvasca  39877  dvavbase  39884  dvafvadd  39885  dvafvsca  39887  diafval  39902  diaval  39903  dvhsca  39953  dvhvbase  39958  dvhfvadd  39962  dvhfvsca  39971  docafvalN  39993  docavalN  39994  djafvalN  40005  djavalN  40006  dibfval  40012  dibopelvalN  40014  dibopelval2  40016  dibelval3  40018  diblsmopel  40042  dicfval  40046  dicval  40047  cdlemn11a  40078  dihvalcqpre  40106  dihopelvalcpre  40119  dihord6apre  40127  dihpN  40207  dochfval  40221  dochval  40222  djhfval  40268  djhval  40269  islpolN  40354  lpolconN  40358  dochpolN  40361  lcfrlem9  40421  lcd0vvalN  40484  mapdval  40499  mapd1o  40519  mapdunirnN  40521  mapdhval  40595  mapdhval0  40596  hvmapfval  40630  hvmapval  40631  hdmap1fval  40667  hdmap1vallem  40668  hgmapfval  40757  hlhilset  40805  hlhilbase  40807  hlhilplus  40808  hlhilvsca  40822  hlhilip  40823  hlhilnvl  40825  hlhillsm  40831  hlhillcs  40833  frlmfielbas  41074  frlm0vald  41109  evlsval3  41131  evlsbagval  41138  evlselv  41159  fsuppind  41162  fsuppssind  41165  mhpind  41166  mhphf  41169  islssfgi  41814  pwssplit4  41831  frlmpwfi  41840  mendplusgfval  41927  mendmulrfval  41929  mendvscafval  41932  idomrootle  41937  idomodle  41938  deg1mhm  41949  mnringelbased  42973  mnring0g2d  42979  mnringmulrd  42980  mnringmulrcld  42987  dvgrat  43071  uzmptshftfval  43105  climexp  44321  climinf  44322  climneg  44326  climdivf  44328  climconstmpt  44374  climresmpt  44375  climsubmpt  44376  fnlimfvre  44390  limsupvaluz  44424  limsupequzmpt2  44434  climuzlem  44459  climisp  44462  climxrrelem  44465  climxrre  44466  limsupgtlem  44493  liminflelimsupuz  44501  liminfgelimsupuz  44504  liminfequzmpt2  44507  liminfvaluz  44508  limsupvaluz3  44514  climliminflimsupd  44517  liminfreuzlem  44518  liminfltlem  44520  liminflimsupclim  44523  liminflbuz2  44531  liminfpnfuz  44532  xlimclim2lem  44555  climxlim2  44562  sge0isum  45143  sge0uzfsumgt  45160  sge0seq  45162  meaiunlelem  45184  caragendifcl  45230  omeiunle  45233  omeiunltfirp  45235  carageniuncl  45239  caragensal  45241  opnssborel  45351  smflimlem6  45492  smfpimcc  45524  smflimmpt  45526  smflimsuplem4  45539  smflimsuplem6  45541  smflimsuplem8  45543  smfliminflem  45546  isomuspgrlem2  46501  ushrisomgr  46509  upwlksfval  46513  isupwlkg  46515  ismgmhm  46553  issubmgm2  46560  submgmacs  46574  copisnmnd  46579  0ringdif  46644  rnghmval  46689  isrnghm  46690  c0snmgmhm  46713  c0snmhm  46714  zrrnghm  46716  rnglidl0  46752  zlidlring  46826  cznrng  46853  cznnring  46854  rngchomfvalALTV  46882  rngccofvalALTV  46885  rngccatidALTV  46887  ringchomfvalALTV  46945  ringccofvalALTV  46948  ringccatidALTV  46950  rngcrescrhm  46983  rngcrescrhmALTV  47001  ofaddmndmap  47019  suppmptcfin  47055  mptcfsupp  47056  dmatALTbas  47082  lcoop  47092  linccl  47095  lcosn0  47101  lincvalsc0  47102  lcoc0  47103  linc0scn0  47104  linc1  47106  lincscmcl  47113  islinindfis  47130  lincext1  47135  lincext2  47136  lindslinindimp2lem2  47140  lindslinindimp2lem3  47141  lindsrng01  47149  snlindsntorlem  47151  snlindsntor  47152  ldepspr  47154  lincresunit1  47158  lincresunit2  47159  lines  47417  line  47418  rrxlines  47419  sphere  47433  rrxsphere  47434  functhinclem1  47661  thincciso  47669