Theorem fvexi 6836

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-fv 6490

This theorem is referenced by:  mptfvmpt  7164  ovex  7382  mapfienlem1  9295  climle  15547  climsup  15577  iserabs  15722  isumshft  15746  explecnv  15772  prodfclim1  15800  ressbas  17147  ressbas2  17149  ressid  17155  ressval3d  17157  topnid  17339  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdsip  17365  prdsle  17366  prdsds  17368  prdshom  17371  prdsco  17372  pwselbasb  17392  pwsvscafval  17398  pwssca  17400  pwssnf1o  17402  imassca  17423  imasvsca  17424  imasle  17427  xpsrnbas  17475  xpssca  17480  xpsvsca  17481  isacs2  17559  homffval  17596  comfffval  17604  oppchomfval  17620  oppccofval  17622  oppccatid  17625  monfval  17639  oppcmon  17645  sectffval  17657  invffval  17665  rescbas  17736  reschom  17737  rescco  17739  fullsubc  17757  isfunc  17771  isfuncd  17772  idfu2nd  17784  idfu1st  17786  cofu1st  17790  cofu2nd  17792  fucco  17872  fucid  17881  invfuc  17884  initoval  17900  termoval  17901  homafval  17936  arwval  17950  coafval  17971  coapm  17978  setccatid  17991  catchomfval  18009  catccofval  18011  catccatid  18013  elestrchom  18034  estrccatid  18038  xpcbas  18084  xpchomfval  18085  xpccofval  18088  1stf1  18098  1stf2  18099  2ndf1  18101  2ndf2  18102  prf1  18106  prf2fval  18107  evlf2  18124  evlf1  18126  curf1fval  18130  curf11  18132  curf12  18133  curf1cl  18134  curf2  18135  curf2cl  18137  hof2fval  18161  yonedalem4a  18181  yonedalem4c  18183  yonedalem3  18186  yonedainv  18187  oduprs  18206  isdrs  18207  ispos  18220  odupos  18232  pltfval  18235  lubfval  18254  lubeldm  18257  lubval  18260  glbfval  18267  glbeldm  18270  glbval  18273  odulub  18311  odujoin  18312  oduglb  18313  odumeet  18314  clatlem  18408  clatlubcl2  18410  clatglbcl2  18412  isdlat  18428  ipolt  18441  ipopos  18442  isacs4lem  18450  plusffval  18520  issstrmgm  18527  gsumvalx  18550  gsumval  18551  ismgmhm  18570  issubmgm2  18577  submgmacs  18591  issubmnd  18635  ress0g  18636  ismhm  18659  mndvcl  18671  0subm  18691  0mhm  18693  submacs  18701  pwsdiagmhm  18705  gsumz  18710  frmdplusg  18728  efmndplusg  18754  efmndmgm  18759  smndex1mgm  18781  grpinvfval  18857  grpsubfval  18862  grpsubfvalALT  18863  mulgfval  18948  mulgfvalALT  18949  mulgval  18950  issubg  19005  0subg  19030  0subgOLD  19031  subgacs  19040  nsgacs  19041  nmznsg  19047  eqgfval  19055  isghm  19094  isghmOLD  19095  gicen  19157  isga  19170  subgga  19179  orbstafun  19190  orbstaval  19191  orbsta  19192  cntzfval  19199  cntzval  19200  oppgplusfval  19227  oppglt  19247  symg2bas  19272  symgvalstruct  19276  cayleylem2  19292  psgnfval  19379  odfval  19411  odinf  19442  dfod2  19443  0subgALT  19447  pgpfi1  19474  pgp0  19475  sylow1lem2  19478  sylow3lem6  19511  lsmfval  19517  lsmvalx  19518  oppglsm  19521  pj1fval  19573  efglem  19595  efgrelexlemb  19629  efgcpbllemb  19634  frgpeccl  19640  frgpmhm  19644  vrgpval  19646  frgpuplem  19651  frgpupf  19652  frgpupval  19653  frgpup1  19654  frgpup3lem  19656  frgpnabllem2  19753  iscygodd  19767  prmcyg  19773  lt6abl  19774  gsumval3a  19782  gsumval3  19786  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumreidx  19796  gsumzaddlem  19800  gsumzadd  19801  gsumzsplit  19806  gsummptshft  19815  gsumzmhm  19816  gsumzoppg  19823  gsumzinv  19824  gsummptfidminv  19826  gsumsub  19827  gsumpt  19841  gsummptf1o  19842  gsum2dlem1  19849  gsum2dlem2  19850  gsum2d  19851  gsum2d2lem  19852  gsumxp2  19859  fsfnn0gsumfsffz  19862  nn0gsumfz  19863  gsummptnn0fz  19865  dprdfid  19898  dprdfinv  19900  dprdfadd  19901  dprdfeq0  19903  dmdprdsplitlem  19918  dpjidcl  19939  ablfacrplem  19946  ablfacrp  19947  ablfacrp2  19948  ablfac1a  19950  ablfac1b  19951  ablfac1c  19952  ablfac1eu  19954  pgpfaclem2  19963  ablfaclem2  19967  ablfaclem3  19968  2nsgsimpgd  19983  prmgrpsimpgd  19995  ablsimpgprmd  19996  mgpplusg  20029  mgpress  20035  issrg  20073  ring1ne0  20184  gsumdixp  20204  pwsmgp  20212  opprmulfval  20224  dvdsrval  20246  isunit  20258  unitgrp  20268  unitlinv  20278  unitrinv  20279  dvrfval  20287  rdivmuldivd  20298  rnghmval  20325  isrnghm  20326  c0snmgmhm  20347  c0snmhm  20348  isnzr2  20403  isnzr2hash  20404  0ring  20411  0ringdif  20412  01eq0ringOLD  20416  0ring01eqbi  20417  zrrnghm  20421  issubrg  20456  subrgugrp  20476  rngcrescrhm  20569  rrgval  20582  rrgsupp  20586  isdrng2  20628  drngmclOLD  20636  drngid2  20637  imadrhmcl  20682  subrgacs  20685  sdrgacs  20686  cntzsdrg  20687  subdrgint  20688  isabv  20696  staffval  20726  ofldlt1  20760  islmod  20767  scaffval  20783  lcomfsupp  20805  mptscmfsupp0  20830  rmodislmod  20833  lssset  20836  islss  20837  lsssn0  20851  lssacs  20870  lspfval  20876  lspval  20878  lspcl  20879  lspuni0  20913  lss0v  20920  0lmhm  20944  lmhmvsca  20949  islbs  20980  islbs3  21062  lbsextlem1  21065  lbsextlem3  21067  lbsextlem4  21068  lbsext  21070  rnglidl0  21136  rsp1  21144  2idlval  21158  qusrhm  21183  expghm  21382  zrhrhmb  21417  zlmvsca  21428  zntoslem  21463  znfi  21466  znunithash  21471  psgnghm  21487  psgnghm2  21488  psgnevpmb  21494  ipffval  21555  ocvfval  21573  ocvval  21574  elocv  21575  thlbas  21603  thlle  21604  thlleval  21605  thloc  21606  pjfval  21613  pjdm  21614  pjpm  21615  isobs  21627  frlmbas  21662  frlmbasf  21667  frlmvscafval  21673  frlmvscavalb  21677  frlmsslss2  21682  frlmip  21685  uvcvval  21693  uvcvvcl  21694  frlmssuvc2  21702  frlmsslsp  21703  ellspd  21709  elfilspd  21710  islinds2  21720  islindf4  21745  aspval  21780  psrbas  21840  psrelbas  21841  psrplusg  21843  psrmulr  21849  psrvscafval  21855  psrvscacl  21858  psr0lid  21860  psrlidm  21869  psrridm  21870  resspsradd  21882  resspsrmul  21883  resspsrvsca  21884  psrascl  21886  mvrval2  21890  mplsubglem  21906  mpllsslem  21907  mplsubrglem  21911  ressmpladd  21934  ressmplmul  21935  ressmplvsca  21936  mplmon  21940  mplmonmul  21941  mplcoe1  21942  opsrle  21952  opsrtoslem2  21961  mplmon2  21966  evlslem4  21981  psrbagev1  21982  evlslem2  21984  evlslem3  21985  evlsval2  21992  selvval  22020  mhpval  22024  ismhp3  22027  psdfval  22043  coe1sfi  22096  coe1fsupp  22097  mptcoe1fsupp  22098  coe1ae0  22099  ressply1add  22112  ressply1mul  22113  ressply1vsca  22114  gsumply1subr  22116  psropprmul  22120  coe1tmmul2fv  22162  coe1pwmulfv  22164  ply1coe  22183  cply1coe0  22186  cply1coe0bi  22187  gsummoncoe1  22193  evls1fval  22204  evls1val  22205  evls1rhmlem  22206  evls1sca  22208  evls1gsumadd  22209  evls1gsummul  22210  evl1val  22214  evl1fval1lem  22215  fveval1fvcl  22218  evl1sca  22219  evl1var  22221  evl1addd  22226  evl1subd  22227  evl1muld  22228  evl1expd  22230  pf1f  22235  pf1mpf  22237  pf1ind  22240  evl1gsummul  22245  evls1expd  22252  evls1fpws  22254  evls1addd  22256  evls1muld  22257  evls1vsca  22258  rhmply1vr1  22272  mamures  22282  mamucl  22286  mamuvs1  22290  mamuvs2  22291  matbas2d  22308  matecl  22310  mamumat1cl  22324  mat1comp  22325  mamulid  22326  mamurid  22327  mat1ov  22333  matsc  22335  mat1dimelbas  22356  mat1dimmul  22361  mat1f1o  22363  dmatval  22377  dmatmulcl  22385  scmatval  22389  scmatscmiddistr  22393  mavmulcl  22432  1mavmul  22433  marrepfval  22445  marrepeval  22448  marepvfval  22450  submafval  22464  mdetfval  22471  mdetunilem9  22505  mdetuni0  22506  m2detleiblem3  22514  m2detleiblem4  22515  minmar1fval  22531  minmar1eval  22534  symgmatr01  22539  gsummatr01lem3  22542  gsummatr01  22544  smadiadetlem1a  22548  smadiadetlem3  22553  invrvald  22561  cpmat  22594  mat2pmatfval  22608  mat2pmatbas  22611  decpmatfsupp  22654  decpmatmulsumfsupp  22658  pmatcollpw3lem  22668  pmatcollpw3fi1lem2  22672  pm2mpval  22680  mply1topmatcl  22690  chmatval  22714  chpmatfval  22715  chfacffsupp  22741  chfacfscmul0  22743  chfacfscmulfsupp  22744  chfacfpmmul0  22747  chfacfpmmulfsupp  22748  cpmidpmatlem2  22756  cpmadumatpolylem1  22766  imastopn  23605  uzrest  23782  tmdgsum2  23981  distgp  23984  indistgp  23985  snclseqg  24001  tsmsval  24016  tsms0  24027  tsmsres  24029  tsmsxplem1  24038  tsmsxplem2  24039  ussid  24146  isusp  24147  ressust  24149  cnextucn  24188  prdsxmetlem  24254  nrmmetd  24460  nmfval  24474  tngds  24534  tngnm  24537  tngngp2  24538  tngngpd  24539  tngngp  24540  tngngp3  24542  nmo0  24621  xrrest  24694  climcncf  24791  cphsubrglem  25075  cphcjcl  25081  tcphex  25115  ipcau2  25132  cmsss  25249  rrxip  25288  minveclem4a  25328  minveclem4  25330  mbflimsup  25565  mbflim  25567  mdegfval  25965  mdegleb  25967  mdegldg  25969  deg1val  25999  uc1pval  26043  mon1pval  26045  q1pval  26058  r1pval  26061  ply1remlem  26068  ply1rem  26069  fta1glem1  26071  fta1glem2  26072  fta1blem  26074  idomrootle  26076  ig1pval  26079  elqaalem3  26227  ulmcau  26302  ulmdvlem1  26307  ulmdvlem3  26309  mbfulm  26313  itgulm  26315  dchrplusg  27156  dchrmullid  27161  dchrinvcl  27162  dchrptlem2  27174  dchrptlem3  27175  dchrsum2  27177  sumdchr2  27179  dchr2sum  27182  axtgcont1  28413  tgjustc1  28420  tgjustc2  28421  tglowdim1  28445  tgldimor  28447  tgldim0eq  28448  iscgrgd  28458  isismt  28479  tglnfn  28492  tglnunirn  28493  tglngval  28496  legval  28529  ishlg  28547  hlcgrex  28561  hlcgreulem  28562  mirval  28600  midexlem  28637  israg  28642  perpln1  28655  perpln2  28656  isperp  28657  ishpg  28704  midf  28721  ismidb  28723  lmif  28730  islmib  28732  iscgra  28754  isinag  28783  isleag  28792  iseqlg  28812  ttgval  28820  ttgitvval  28827  setsvtx  28980  uhgrunop  29020  incistruhgr  29024  upgrunop  29064  umgrunop  29066  usgriedgleord  29173  uspgredgleord  29177  uhgr0vsize0  29184  lfuhgr1v0e  29199  uhgrspanop  29241  upgrspanop  29242  umgrspanop  29243  usgrspanop  29244  uhgrspan1lem1  29245  upgrres1lem1  29254  usgredgffibi  29269  fusgredgfi  29270  usgr1v0e  29271  nbgr2vtx1edg  29295  nbuhgr2vtx1edgb  29297  nbfusgrlevtxm1  29322  nbfusgrlevtxm2  29323  uvtx01vtx  29342  cplgr1vlem  29374  cplgr1v  29375  cusgrsize2inds  29399  cusgrfilem3  29403  sizusglecusg  29409  fusgrmaxsize  29410  vtxdgfval  29413  vtxdun  29427  vtxd0nedgb  29434  p1evtxdeqlem  29458  p1evtxdeq  29459  p1evtxdp1  29460  usgrvd0nedg  29479  vtxdginducedm1lem1  29485  vtxdginducedm1lem4  29488  vtxdginducedm1  29489  vtxdginducedm1fi  29490  finsumvtxdg2ssteplem4  29494  rusgrnumwrdl2  29532  wksfval  29555  iswlkg  29559  wlkonprop  29602  wlkp1lem3  29619  wlkp1lem8  29624  wlkp1  29625  wksonproplem  29648  wwlks  29780  wwlksnon  29796  wspthsnon  29797  clwwlk  29927  0wlkonlem2  30063  conngrv2edg  30139  eupthp1  30160  eupth2eucrct  30161  eupthvdres  30179  eupth2lem3  30180  eupth2lemb  30181  3cyclfrgrrn  30230  frgrwopreglem1  30256  frgrwopreg1  30262  imsmetlem  30634  dipfval  30646  sspval  30667  islno  30697  nmooval  30707  nmounbseqi  30721  nmobndseqi  30723  0ofval  30731  0oval  30732  ajfval  30753  isph  30766  phpar  30768  ajval  30805  ubthlem1  30814  ubthlem2  30815  minvecolem4b  30822  minvecolem4  30824  minvecolem5  30825  hlex  30842  ressplusf  32905  ressnm  32906  ressprs  32908  ismnt  32925  mgcval  32929  gsummptres  33005  gsummptres2  33006  gsumfs2d  33008  gsumpart  33010  gsumhashmul  33014  gsumwrd2dccat  33020  conjga  33112  inftmrel  33122  isinftm  33123  gsumvsca1  33168  ress1r  33174  ringinvval  33175  dvrcan5  33176  rmfsupp2  33178  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  elrgspn  33186  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  erlval  33198  rlocval  33199  rlocbas  33207  rlocaddval  33208  rlocmulval  33209  rlocf1  33213  fldgenval  33251  resvsca  33270  quslmod  33295  islinds5  33304  ellspds  33305  elrsp  33309  linds2eq  33318  elringlsm  33330  lsmsnpridl  33335  grplsm0l  33340  qusima  33345  nsgmgc  33349  nsgqusf1o  33353  elrspunidl  33365  elrspunsn  33366  drngidlhash  33371  prmidl0  33387  oppreqg  33420  opprqusbas  33425  qsdrngi  33432  idlsrgbas  33441  idlsrgplusg  33442  idlsrgmulr  33444  idlsrgtset  33445  rprmval  33453  1arithidom  33474  fply1  33493  evls1fvf  33497  evl1fvf  33498  coe1zfv  33523  r1pquslmic  33543  mplvrpmfgalem  33545  mplvrpmga  33546  resssra  33553  exsslsb  33563  lbslelsp  33564  dimval  33567  dimvalfi  33568  lvecdim0  33573  ply1degltdimlem  33589  irngval  33652  elirng  33653  irngss  33654  irngnzply1lem  33657  extdgfialglem2  33660  minplyval  33672  constrsuc  33705  constrelextdg2  33714  mdetpmtr1  33790  rspectopn  33834  zarcls0  33835  zarcls  33841  zartopn  33842  zarmxt1  33847  rhmpreimacnlem  33851  rhmpreimacn  33852  pstmfval  33863  ordtrest2NEW  33890  ordtconnlem1  33891  fsumcvg4  33917  pl1cn  33922  qqhval  33939  sibf0  34302  sitgclg  34310  sitgaddlemb  34316  eulerpartlemgvv  34344  afsval  34639  onvf1odlem3  35078  pthhashvtx  35101  usgrcyclgt2v  35104  cusgr3cyclex  35109  acycgr2v  35123  cusgracyclt3v  35129  mrsubfval  35481  mrsubcv  35483  mrsubff  35485  mrsubrn  35486  elmrsubrn  35493  msubfval  35497  msubff  35503  mpstval  35508  elmpst  35509  msrval  35511  mstaval  35517  msubvrs  35533  mclsssvlem  35535  mclsval  35536  mclsind  35543  mppsval  35545  climlec3  35707  sdclem2  37722  sdclem1  37723  caures  37740  heiborlem3  37793  heibor  37801  grpokerinj  37873  rngoi  37879  dvrunz  37934  isdrngo1  37936  isdrngo2  37938  isrngohom  37945  idlval  37993  isidl  37994  0idl  38005  0rngo  38007  divrngidl  38008  smprngopr  38032  igenval  38041  lshpset  38957  lsatset  38969  lcvfbr  38999  islfl  39039  lfl0f  39048  lfl1  39049  lfladd0l  39053  lflnegl  39055  lflvscl  39056  lflvsdi1  39057  lflvsdi2  39058  lflvsdi2a  39059  lflvsass  39060  lfl0sc  39061  lflsc0N  39062  lfl1sc  39063  lkr0f  39073  lkrsc  39076  eqlkr2  39079  ldualvbase  39105  ldualfvadd  39107  ldualvaddval  39110  ldualsca  39111  ldualfvs  39115  ldualvsval  39117  isopos  39159  cmtfvalN  39189  cvrfval  39247  pats  39264  llnset  39484  lplnset  39508  lvolset  39551  lineset  39717  isline  39718  pointsetN  39720  psubspset  39723  ispsubsp  39724  pmapval  39736  paddfval  39776  paddval  39777  pclfvalN  39868  pclvalN  39869  polfvalN  39883  polvalN  39884  psubclsetN  39915  ispsubclN  39916  watvalN  39972  lhpset  39974  lautset  40061  islaut  40062  pautsetN  40077  ispautN  40078  ldilset  40088  ltrnset  40097  dilsetN  40132  cdleme26e  40338  cdleme26eALTN  40340  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme41sn3a  40412  cdleme32a  40420  cdleme40m  40446  cdleme40n  40447  cdleme42b  40457  tgrpbase  40725  tgrpopr  40726  istendo  40739  tendopl  40755  tendo02  40766  erngbase  40780  erngfplus  40781  erngfmul  40784  erngbase-rN  40788  erngfplus-rN  40789  erngfmul-rN  40792  cdlemk36  40892  cdlemkid  40915  dvasca  40985  dvavbase  40992  dvafvadd  40993  dvafvsca  40995  diafval  41010  diaval  41011  dvhsca  41061  dvhvbase  41066  dvhfvadd  41070  dvhfvsca  41079  docafvalN  41101  docavalN  41102  djafvalN  41113  djavalN  41114  dibfval  41120  dibopelvalN  41122  dibopelval2  41124  dibelval3  41126  diblsmopel  41150  dicfval  41154  dicval  41155  cdlemn11a  41186  dihvalcqpre  41214  dihopelvalcpre  41227  dihord6apre  41235  dihpN  41315  dochfval  41329  dochval  41330  djhfval  41376  djhval  41377  islpolN  41462  lpolconN  41466  dochpolN  41469  lcfrlem9  41529  lcd0vvalN  41592  mapdval  41607  mapd1o  41627  mapdunirnN  41629  mapdhval  41703  mapdhval0  41704  hvmapfval  41738  hvmapval  41739  hdmap1fval  41775  hdmap1vallem  41776  hgmapfval  41865  hlhilset  41913  hlhilbase  41915  hlhilplus  41916  hlhilvsca  41926  hlhilip  41927  hlhilnvl  41929  hlhillsm  41935  hlhillcs  41937  hashscontpow  42095  frlmfielbas  42473  fimgmcyc  42507  frlm0vald  42512  evlsval3  42532  evlsbagval  42539  selvcllem5  42555  evlselv  42560  fsuppind  42563  fsuppssind  42566  mhpind  42567  mhphf  42570  sn-isghm  42646  islssfgi  43045  pwssplit4  43062  frlmpwfi  43071  mendplusgfval  43154  mendmulrfval  43156  mendvscafval  43159  idomodle  43164  deg1mhm  43173  mnringelbased  44190  mnring0g2d  44195  mnringmulrd  44196  mnringmulrcld  44201  dvgrat  44285  uzmptshftfval  44319  climexp  45586  climinf  45587  climneg  45591  climdivf  45593  climconstmpt  45639  climresmpt  45640  climsubmpt  45641  fnlimfvre  45655  limsupvaluz  45689  limsupequzmpt2  45699  climuzlem  45724  climisp  45727  climxrrelem  45730  climxrre  45731  limsupgtlem  45758  liminflelimsupuz  45766  liminfgelimsupuz  45769  liminfequzmpt2  45772  liminfvaluz  45773  limsupvaluz3  45779  climliminflimsupd  45782  liminfreuzlem  45783  liminfltlem  45785  liminflimsupclim  45788  liminflbuz2  45796  liminfpnfuz  45797  xlimclim2lem  45820  climxlim2  45827  sge0isum  46408  sge0uzfsumgt  46425  sge0seq  46427  meaiunlelem  46449  caragendifcl  46495  omeiunle  46498  omeiunltfirp  46500  carageniuncl  46504  caragensal  46506  opnssborel  46616  smflimlem6  46757  smfpimcc  46789  smflimmpt  46791  smflimsuplem4  46804  smflimsuplem6  46806  smflimsuplem8  46808  smfliminflem  46811  clnbgrlevtx  47829  isisubgr  47846  isubgriedg  47847  isubgrvtx  47851  isuspgrim  47880  gricen  47909  ushggricedg  47911  uhgrimisgrgric  47915  grtri  47924  isubgr3stgrlem2  47951  grlicen  48001  clnbgr3stgrgrlim  48003  clnbgr3stgrgrlic  48004  upwlksfval  48119  isupwlkg  48121  copisnmnd  48153  zlidlring  48218  cznrng  48245  cznnring  48246  rngchomfvalALTV  48251  rngccofvalALTV  48254  rngccatidALTV  48256  rngcrescrhmALTV  48264  ringchomfvalALTV  48285  ringccofvalALTV  48288  ringccatidALTV  48290  ofaddmndmap  48327  suppmptcfin  48360  mptcfsupp  48361  dmatALTbas  48386  lcoop  48396  linccl  48399  lcosn0  48405  lincvalsc0  48406  lcoc0  48407  linc0scn0  48408  linc1  48410  lincscmcl  48417  islinindfis  48434  lincext1  48439  lincext2  48440  lindslinindimp2lem2  48444  lindslinindimp2lem3  48445  lindsrng01  48453  snlindsntorlem  48455  snlindsntor  48456  ldepspr  48458  lincresunit1  48462  lincresunit2  48463  lines  48716  line  48717  rrxlines  48718  sphere  48732  rrxsphere  48733  discsubc  49049  nelsubclem  49052  funcf2lem2  49067  cofidvala  49101  cofidval  49104  upfval  49161  upfval2  49162  isnatd  49208  swapf2fvala  49249  swapf1vala  49251  tposcurf1  49284  diag1f1lem  49291  fuco112  49314  functhinclem1  49429  thincciso  49438  oppcterm  49491  functermc2  49494  idfudiag1bas  49509  idfudiag1  49510  cmddu  49653