Theorem fvexi 6920

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ‘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  ax-nul 5311

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

This theorem is referenced by:  mptfvmpt  7247  ovex  7463  mapfienlem1  9442  climle  15672  climsup  15702  iserabs  15847  isumshft  15871  explecnv  15897  prodfclim1  15925  ressbas  17279  ressbasOLD  17280  ressbas2  17282  ressid  17289  ressval3d  17291  ressval3dOLD  17292  topnid  17481  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdsip  17507  prdsle  17508  prdsds  17510  prdshom  17513  prdsco  17514  pwselbasb  17534  pwsvscafval  17540  pwssca  17542  pwssnf1o  17544  imassca  17565  imasvsca  17566  imasle  17569  xpsrnbas  17617  xpssca  17622  xpsvsca  17623  isacs2  17697  homffval  17734  comfffval  17742  oppchomfval  17758  oppchomfvalOLD  17759  oppccofval  17761  oppccatid  17765  monfval  17779  oppcmon  17785  sectffval  17797  invffval  17805  rescbas  17876  rescbasOLD  17877  reschom  17878  rescco  17880  resccoOLD  17881  fullsubc  17900  isfunc  17914  isfuncd  17915  idfu2nd  17927  idfu1st  17929  cofu1st  17933  cofu2nd  17935  fucco  18018  fucid  18027  invfuc  18030  initoval  18046  termoval  18047  homafval  18082  arwval  18096  coafval  18117  coapm  18124  setccatid  18137  catchomfval  18155  catccofval  18157  catccatid  18159  elestrchom  18182  estrccatid  18186  xpcbas  18233  xpchomfval  18234  xpccofval  18237  1stf1  18247  1stf2  18248  2ndf1  18250  2ndf2  18251  prf1  18255  prf2fval  18256  evlf2  18274  evlf1  18276  curf1fval  18280  curf11  18282  curf12  18283  curf1cl  18284  curf2  18285  curf2cl  18287  hof2fval  18311  yonedalem4a  18331  yonedalem4c  18333  yonedalem3  18336  yonedainv  18337  oduprs  18357  isdrs  18358  ispos  18371  odupos  18385  pltfval  18388  lubfval  18407  lubeldm  18410  lubval  18413  glbfval  18420  glbeldm  18423  glbval  18426  odulub  18464  odujoin  18465  oduglb  18466  odumeet  18467  clatlem  18559  clatlubcl2  18561  clatglbcl2  18563  isdlat  18579  ipolt  18592  ipopos  18593  isacs4lem  18601  plusffval  18671  issstrmgm  18678  gsumvalx  18701  gsumval  18702  ismgmhm  18721  issubmgm2  18728  submgmacs  18742  issubmnd  18786  ress0g  18787  ismhm  18810  mndvcl  18822  0subm  18842  0mhm  18844  submacs  18852  pwsdiagmhm  18856  gsumz  18861  frmdplusg  18879  efmndplusg  18905  efmndmgm  18910  smndex1mgm  18932  grpinvfval  19008  grpsubfval  19013  grpsubfvalALT  19014  mulgfval  19099  mulgfvalALT  19100  mulgval  19101  issubg  19156  0subg  19181  0subgOLD  19182  subgacs  19191  nsgacs  19192  nmznsg  19198  eqgfval  19206  isghm  19245  isghmOLD  19246  gicen  19308  isga  19321  subgga  19330  orbstafun  19341  orbstaval  19342  orbsta  19343  cntzfval  19350  cntzval  19351  oppgplusfval  19378  symg2bas  19424  symgvalstruct  19428  symgvalstructOLD  19429  cayleylem2  19445  psgnfval  19532  odfval  19564  odinf  19595  dfod2  19596  0subgALT  19600  pgpfi1  19627  pgp0  19628  sylow1lem2  19631  sylow3lem6  19664  lsmfval  19670  lsmvalx  19671  oppglsm  19674  pj1fval  19726  efglem  19748  efgrelexlemb  19782  efgcpbllemb  19787  frgpeccl  19793  frgpmhm  19797  vrgpval  19799  frgpuplem  19804  frgpupf  19805  frgpupval  19806  frgpup1  19807  frgpup3lem  19809  frgpnabllem2  19906  iscygodd  19920  prmcyg  19926  lt6abl  19927  gsumval3a  19935  gsumval3  19939  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumreidx  19949  gsumzaddlem  19953  gsumzadd  19954  gsumzsplit  19959  gsummptshft  19968  gsumzmhm  19969  gsumzoppg  19976  gsumzinv  19977  gsummptfidminv  19979  gsumsub  19980  gsumpt  19994  gsummptf1o  19995  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  gsum2d2lem  20005  gsumxp2  20012  fsfnn0gsumfsffz  20015  nn0gsumfz  20016  gsummptnn0fz  20018  dprdfid  20051  dprdfinv  20053  dprdfadd  20054  dprdfeq0  20056  dmdprdsplitlem  20071  dpjidcl  20092  ablfacrplem  20099  ablfacrp  20100  ablfacrp2  20101  ablfac1a  20103  ablfac1b  20104  ablfac1c  20105  ablfac1eu  20107  pgpfaclem2  20116  ablfaclem2  20120  ablfaclem3  20121  2nsgsimpgd  20136  prmgrpsimpgd  20148  ablsimpgprmd  20149  mgpplusg  20155  mgpress  20166  mgpressOLD  20167  issrg  20205  ring1ne0  20312  gsumdixp  20332  pwsmgp  20340  opprmulfval  20352  dvdsrval  20377  isunit  20389  unitgrp  20399  unitlinv  20409  unitrinv  20410  dvrfval  20418  rdivmuldivd  20429  rnghmval  20456  isrnghm  20457  c0snmgmhm  20478  c0snmhm  20479  isnzr2  20534  isnzr2hash  20535  0ring  20542  0ringdif  20543  01eq0ringOLD  20547  0ring01eqbi  20548  zrrnghm  20552  issubrg  20587  subrgugrp  20607  rngcrescrhm  20700  rrgval  20713  rrgsupp  20717  isdrng2  20759  drngmclOLD  20767  drngid2  20768  imadrhmcl  20814  subrgacs  20817  sdrgacs  20818  cntzsdrg  20819  subdrgint  20820  isabv  20828  staffval  20858  islmod  20878  scaffval  20894  lcomfsupp  20916  mptscmfsupp0  20941  rmodislmod  20944  rmodislmodOLD  20945  lssset  20948  islss  20949  lsssn0  20963  lssacs  20982  lspfval  20988  lspval  20990  lspcl  20991  lspuni0  21025  lss0v  21032  0lmhm  21056  lmhmvsca  21061  islbs  21092  islbs3  21174  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  lbsext  21182  rnglidl0  21256  rsp1  21264  2idlval  21278  qusrhm  21303  expghm  21503  zrhrhmb  21538  zlmvsca  21553  zntoslem  21592  znfi  21595  znunithash  21600  psgnghm  21615  psgnghm2  21616  psgnevpmb  21622  ipffval  21683  ocvfval  21701  ocvval  21702  elocv  21703  thlbas  21731  thlbasOLD  21732  thlle  21733  thlleOLD  21734  thlleval  21735  thloc  21736  pjfval  21743  pjdm  21744  pjpm  21745  isobs  21757  frlmbas  21792  frlmbasf  21797  frlmvscafval  21803  frlmvscavalb  21807  frlmsslss2  21812  frlmip  21815  uvcvval  21823  uvcvvcl  21824  frlmssuvc2  21832  frlmsslsp  21833  ellspd  21839  elfilspd  21840  islinds2  21850  islindf4  21875  aspval  21910  psrbas  21970  psrelbas  21971  psrplusg  21973  psrmulr  21979  psrvscafval  21985  psrvscacl  21988  psr0lid  21990  psrlidm  21999  psrridm  22000  resspsradd  22012  resspsrmul  22013  resspsrvsca  22014  psrascl  22016  mvrval2  22020  mplsubglem  22036  mpllsslem  22037  mplsubrglem  22041  ressmpladd  22064  ressmplmul  22065  ressmplvsca  22066  mplmon  22070  mplmonmul  22071  mplcoe1  22072  opsrle  22082  opsrtoslem2  22097  mplmon2  22102  evlslem4  22117  psrbagev1  22118  evlslem2  22120  evlslem3  22121  evlsval2  22128  selvval  22156  mhpval  22160  ismhp3  22163  psdfval  22179  coe1sfi  22230  coe1fsupp  22231  mptcoe1fsupp  22232  coe1ae0  22233  ressply1add  22246  ressply1mul  22247  ressply1vsca  22248  gsumply1subr  22250  psropprmul  22254  coe1tmmul2fv  22296  coe1pwmulfv  22298  ply1coe  22317  cply1coe0  22320  cply1coe0bi  22321  gsummoncoe1  22327  evls1fval  22338  evls1val  22339  evls1rhmlem  22340  evls1sca  22342  evls1gsumadd  22343  evls1gsummul  22344  evl1val  22348  evl1fval1lem  22349  fveval1fvcl  22352  evl1sca  22353  evl1var  22355  evl1addd  22360  evl1subd  22361  evl1muld  22362  evl1expd  22364  pf1f  22369  pf1mpf  22371  pf1ind  22374  evl1gsummul  22379  evls1expd  22386  evls1fpws  22388  evls1addd  22390  evls1muld  22391  evls1vsca  22392  rhmply1vr1  22406  mamures  22416  mamucl  22420  mamuvs1  22424  mamuvs2  22425  matbas2d  22444  matecl  22446  mamumat1cl  22460  mat1comp  22461  mamulid  22462  mamurid  22463  mat1ov  22469  matsc  22471  mat1dimelbas  22492  mat1dimmul  22497  mat1f1o  22499  dmatval  22513  dmatmulcl  22521  scmatval  22525  scmatscmiddistr  22529  mavmulcl  22568  1mavmul  22569  marrepfval  22581  marrepeval  22584  marepvfval  22586  submafval  22600  mdetfval  22607  mdetunilem9  22641  mdetuni0  22642  m2detleiblem3  22650  m2detleiblem4  22651  minmar1fval  22667  minmar1eval  22670  symgmatr01  22675  gsummatr01lem3  22678  gsummatr01  22680  smadiadetlem1a  22684  smadiadetlem3  22689  invrvald  22697  cpmat  22730  mat2pmatfval  22744  mat2pmatbas  22747  decpmatfsupp  22790  decpmatmulsumfsupp  22794  pmatcollpw3lem  22804  pmatcollpw3fi1lem2  22808  pm2mpval  22816  mply1topmatcl  22826  chmatval  22850  chpmatfval  22851  chfacffsupp  22877  chfacfscmul0  22879  chfacfscmulfsupp  22880  chfacfpmmul0  22883  chfacfpmmulfsupp  22884  cpmidpmatlem2  22892  cpmadumatpolylem1  22902  imastopn  23743  uzrest  23920  tmdgsum2  24119  distgp  24122  indistgp  24123  snclseqg  24139  tsmsval  24154  tsms0  24165  tsmsres  24167  tsmsxplem1  24176  tsmsxplem2  24177  ussid  24284  isusp  24285  ressust  24287  cnextucn  24327  prdsxmetlem  24393  nrmmetd  24602  nmfval  24616  tngds  24683  tngdsOLD  24684  tngnm  24687  tngngp2  24688  tngngpd  24689  tngngp  24690  tngngp3  24692  nmo0  24771  xrrest  24842  climcncf  24939  cphsubrglem  25224  cphcjcl  25230  tcphex  25264  ipcau2  25281  cmsss  25398  rrxip  25437  minveclem4a  25477  minveclem4  25479  mbflimsup  25714  mbflim  25716  mdegfval  26115  mdegleb  26117  mdegldg  26119  deg1val  26149  uc1pval  26193  mon1pval  26195  q1pval  26208  r1pval  26211  ply1remlem  26218  ply1rem  26219  fta1glem1  26221  fta1glem2  26222  fta1blem  26224  idomrootle  26226  ig1pval  26229  elqaalem3  26377  ulmcau  26452  ulmdvlem1  26457  ulmdvlem3  26459  mbfulm  26463  itgulm  26465  dchrplusg  27305  dchrmullid  27310  dchrinvcl  27311  dchrptlem2  27323  dchrptlem3  27324  dchrsum2  27326  sumdchr2  27328  dchr2sum  27331  axtgcont1  28490  tgjustc1  28497  tgjustc2  28498  tglowdim1  28522  tgldimor  28524  tgldim0eq  28525  iscgrgd  28535  isismt  28556  tglnfn  28569  tglnunirn  28570  tglngval  28573  legval  28606  ishlg  28624  hlcgrex  28638  hlcgreulem  28639  mirval  28677  midexlem  28714  israg  28719  perpln1  28732  perpln2  28733  isperp  28734  ishpg  28781  midf  28798  ismidb  28800  lmif  28807  islmib  28809  iscgra  28831  isinag  28860  isleag  28869  iseqlg  28889  ttgval  28897  ttgvalOLD  28898  ttgitvval  28910  setsvtx  29066  uhgrunop  29106  incistruhgr  29110  upgrunop  29150  umgrunop  29152  usgriedgleord  29259  uspgredgleord  29263  uhgr0vsize0  29270  lfuhgr1v0e  29285  uhgrspanop  29327  upgrspanop  29328  umgrspanop  29329  usgrspanop  29330  uhgrspan1lem1  29331  upgrres1lem1  29340  usgredgffibi  29355  fusgredgfi  29356  usgr1v0e  29357  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nbfusgrlevtxm1  29408  nbfusgrlevtxm2  29409  uvtx01vtx  29428  cplgr1vlem  29460  cplgr1v  29461  cusgrsize2inds  29485  cusgrfilem3  29489  sizusglecusg  29495  fusgrmaxsize  29496  vtxdgfval  29499  vtxdun  29513  vtxd0nedgb  29520  p1evtxdeqlem  29544  p1evtxdeq  29545  p1evtxdp1  29546  usgrvd0nedg  29565  vtxdginducedm1lem1  29571  vtxdginducedm1lem4  29574  vtxdginducedm1  29575  vtxdginducedm1fi  29576  finsumvtxdg2ssteplem4  29580  rusgrnumwrdl2  29618  wksfval  29641  iswlkg  29645  wlkonprop  29690  wlkp1lem3  29707  wlkp1lem8  29712  wlkp1  29713  wksonproplem  29736  wksonproplemOLD  29737  wwlks  29864  wwlksnon  29880  wspthsnon  29881  clwwlk  30011  0wlkonlem2  30147  conngrv2edg  30223  eupthp1  30244  eupth2eucrct  30245  eupthvdres  30263  eupth2lem3  30264  eupth2lemb  30265  3cyclfrgrrn  30314  frgrwopreglem1  30340  frgrwopreg1  30346  imsmetlem  30718  dipfval  30730  sspval  30751  islno  30781  nmooval  30791  nmounbseqi  30805  nmobndseqi  30807  0ofval  30815  0oval  30816  ajfval  30837  isph  30850  phpar  30852  ajval  30889  ubthlem1  30898  ubthlem2  30899  minvecolem4b  30906  minvecolem4  30908  minvecolem5  30909  hlex  30926  ressplusf  32932  ressnm  32933  oppglt  32937  ressprs  32938  ismnt  32957  mgcval  32961  gsummptres  33037  gsummptres2  33038  gsumfs2d  33040  gsumpart  33042  gsumhashmul  33046  gsumwrd2dccat  33052  inftmrel  33169  isinftm  33170  gsumvsca1  33214  ress1r  33223  ringinvval  33224  dvrcan5  33225  rmfsupp2  33227  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  erlval  33244  rlocval  33245  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  rlocf1  33259  fldgenval  33293  ofldlt1  33322  resvsca  33335  quslmod  33365  islinds5  33374  ellspds  33375  elrsp  33379  linds2eq  33388  elringlsm  33400  lsmsnpridl  33405  grplsm0l  33410  qusima  33415  nsgmgc  33419  nsgqusf1o  33423  elrspunidl  33435  elrspunsn  33436  drngidlhash  33441  prmidl0  33457  oppreqg  33490  opprqusbas  33495  qsdrngi  33502  idlsrgbas  33511  idlsrgplusg  33512  idlsrgmulr  33514  idlsrgtset  33515  rprmval  33523  1arithidom  33544  fply1  33563  evls1fvf  33567  evl1fvf  33568  coe1zfv  33591  r1pquslmic  33610  resssra  33616  dimval  33627  dimvalfi  33628  lvecdim0  33633  ply1degltdimlem  33649  irngval  33699  elirng  33700  irngss  33701  irngnzply1lem  33704  minplyval  33712  constrsuc  33742  constrelextdg2  33751  mdetpmtr1  33783  rspectopn  33827  zarcls0  33828  zarcls  33834  zartopn  33835  zarmxt1  33840  rhmpreimacnlem  33844  rhmpreimacn  33845  pstmfval  33856  ordtrest2NEW  33883  ordtconnlem1  33884  fsumcvg4  33910  pl1cn  33915  qqhval  33934  sibf0  34315  sitgclg  34323  sitgaddlemb  34329  eulerpartlemgvv  34357  afsval  34664  pthhashvtx  35111  usgrcyclgt2v  35115  cusgr3cyclex  35120  acycgr2v  35134  cusgracyclt3v  35140  mrsubfval  35492  mrsubcv  35494  mrsubff  35496  mrsubrn  35497  elmrsubrn  35504  msubfval  35508  msubff  35514  mpstval  35519  elmpst  35520  msrval  35522  mstaval  35528  msubvrs  35544  mclsssvlem  35546  mclsval  35547  mclsind  35554  mppsval  35556  climlec3  35713  sdclem2  37728  sdclem1  37729  caures  37746  heiborlem3  37799  heibor  37807  grpokerinj  37879  rngoi  37885  dvrunz  37940  isdrngo1  37942  isdrngo2  37944  isrngohom  37951  idlval  37999  isidl  38000  0idl  38011  0rngo  38013  divrngidl  38014  smprngopr  38038  igenval  38047  lshpset  38959  lsatset  38971  lcvfbr  39001  islfl  39041  lfl0f  39050  lfl1  39051  lfladd0l  39055  lflnegl  39057  lflvscl  39058  lflvsdi1  39059  lflvsdi2  39060  lflvsdi2a  39061  lflvsass  39062  lfl0sc  39063  lflsc0N  39064  lfl1sc  39065  lkr0f  39075  lkrsc  39078  eqlkr2  39081  ldualvbase  39107  ldualfvadd  39109  ldualvaddval  39112  ldualsca  39113  ldualfvs  39117  ldualvsval  39119  isopos  39161  cmtfvalN  39191  cvrfval  39249  pats  39266  glbconNOLD  39359  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  isline  39721  pointsetN  39723  psubspset  39726  ispsubsp  39727  pmapval  39739  paddfval  39779  paddval  39780  pclfvalN  39871  pclvalN  39872  polfvalN  39886  polvalN  39887  psubclsetN  39918  ispsubclN  39919  watvalN  39975  lhpset  39977  lautset  40064  islaut  40065  pautsetN  40080  ispautN  40081  ldilset  40091  ltrnset  40100  dilsetN  40135  cdleme26e  40341  cdleme26eALTN  40343  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32a  40423  cdleme40m  40449  cdleme40n  40450  cdleme42b  40460  tgrpbase  40728  tgrpopr  40729  istendo  40742  tendopl  40758  tendo02  40769  erngbase  40783  erngfplus  40784  erngfmul  40787  erngbase-rN  40791  erngfplus-rN  40792  erngfmul-rN  40795  cdlemk36  40895  cdlemkid  40918  dvasca  40988  dvavbase  40995  dvafvadd  40996  dvafvsca  40998  diafval  41013  diaval  41014  dvhsca  41064  dvhvbase  41069  dvhfvadd  41073  dvhfvsca  41082  docafvalN  41104  docavalN  41105  djafvalN  41116  djavalN  41117  dibfval  41123  dibopelvalN  41125  dibopelval2  41127  dibelval3  41129  diblsmopel  41153  dicfval  41157  dicval  41158  cdlemn11a  41189  dihvalcqpre  41217  dihopelvalcpre  41230  dihord6apre  41238  dihpN  41318  dochfval  41332  dochval  41333  djhfval  41379  djhval  41380  islpolN  41465  lpolconN  41469  dochpolN  41472  lcfrlem9  41532  lcd0vvalN  41595  mapdval  41610  mapd1o  41630  mapdunirnN  41632  mapdhval  41706  mapdhval0  41707  hvmapfval  41741  hvmapval  41742  hdmap1fval  41778  hdmap1vallem  41779  hgmapfval  41868  hlhilset  41916  hlhilbase  41918  hlhilplus  41919  hlhilvsca  41933  hlhilip  41934  hlhilnvl  41936  hlhillsm  41942  hlhillcs  41944  hashscontpow  42103  frlmfielbas  42486  fimgmcyc  42520  frlm0vald  42525  evlsval3  42545  evlsbagval  42552  selvcllem5  42568  evlselv  42573  fsuppind  42576  fsuppssind  42579  mhpind  42580  mhphf  42583  sn-isghm  42659  islssfgi  43060  pwssplit4  43077  frlmpwfi  43086  mendplusgfval  43169  mendmulrfval  43171  mendvscafval  43174  idomodle  43179  deg1mhm  43188  mnringelbased  44209  mnring0g2d  44215  mnringmulrd  44216  mnringmulrcld  44223  dvgrat  44307  uzmptshftfval  44341  climexp  45560  climinf  45561  climneg  45565  climdivf  45567  climconstmpt  45613  climresmpt  45614  climsubmpt  45615  fnlimfvre  45629  limsupvaluz  45663  limsupequzmpt2  45673  climuzlem  45698  climisp  45701  climxrrelem  45704  climxrre  45705  limsupgtlem  45732  liminflelimsupuz  45740  liminfgelimsupuz  45743  liminfequzmpt2  45746  liminfvaluz  45747  limsupvaluz3  45753  climliminflimsupd  45756  liminfreuzlem  45757  liminfltlem  45759  liminflimsupclim  45762  liminflbuz2  45770  liminfpnfuz  45771  xlimclim2lem  45794  climxlim2  45801  sge0isum  46382  sge0uzfsumgt  46399  sge0seq  46401  meaiunlelem  46423  caragendifcl  46469  omeiunle  46472  omeiunltfirp  46474  carageniuncl  46478  caragensal  46480  opnssborel  46590  smflimlem6  46731  smfpimcc  46763  smflimmpt  46765  smflimsuplem4  46778  smflimsuplem6  46780  smflimsuplem8  46782  smfliminflem  46785  clnbgrlevtx  47768  isisubgr  47785  isubgriedg  47786  isubgrvtx  47790  uspgrimprop  47810  isuspgrim  47812  gricen  47831  ushggricedg  47833  uhgrimisgrgric  47836  grtri  47844  isubgr3stgrlem2  47869  grlicen  47912  clnbgr3stgrgrlic  47914  upwlksfval  47978  isupwlkg  47980  copisnmnd  48012  zlidlring  48077  cznrng  48104  cznnring  48105  rngchomfvalALTV  48110  rngccofvalALTV  48113  rngccatidALTV  48115  rngcrescrhmALTV  48123  ringchomfvalALTV  48144  ringccofvalALTV  48147  ringccatidALTV  48149  ofaddmndmap  48187  suppmptcfin  48220  mptcfsupp  48221  dmatALTbas  48246  lcoop  48256  linccl  48259  lcosn0  48265  lincvalsc0  48266  lcoc0  48267  linc0scn0  48268  linc1  48270  lincscmcl  48277  islinindfis  48294  lincext1  48299  lincext2  48300  lindslinindimp2lem2  48304  lindslinindimp2lem3  48305  lindsrng01  48313  snlindsntorlem  48315  snlindsntor  48316  ldepspr  48318  lincresunit1  48322  lincresunit2  48323  lines  48580  line  48581  rrxlines  48582  sphere  48596  rrxsphere  48597  functhinclem1  48840  thincciso  48848