Theorem fvexi 6842

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ‘cfv 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-sn 4576  df-pr 4578  df-uni 4859  df-iota 6443  df-fv 6495

This theorem is referenced by:  mptfvmpt  7168  ovex  7385  mapfienlem1  9295  climle  15553  climsup  15583  iserabs  15728  isumshft  15752  explecnv  15778  prodfclim1  15806  ressbas  17153  ressbas2  17155  ressid  17161  ressval3d  17163  topnid  17345  prdsplusg  17368  prdsmulr  17369  prdsvsca  17370  prdsip  17371  prdsle  17372  prdsds  17374  prdshom  17377  prdsco  17378  pwselbasb  17398  pwsvscafval  17404  pwssca  17406  pwssnf1o  17408  imassca  17429  imasvsca  17430  imasle  17433  xpsrnbas  17481  xpssca  17486  xpsvsca  17487  isacs2  17565  homffval  17602  comfffval  17610  oppchomfval  17626  oppccofval  17628  oppccatid  17631  monfval  17645  oppcmon  17651  sectffval  17663  invffval  17671  rescbas  17742  reschom  17743  rescco  17745  fullsubc  17763  isfunc  17777  isfuncd  17778  idfu2nd  17790  idfu1st  17792  cofu1st  17796  cofu2nd  17798  fucco  17878  fucid  17887  invfuc  17890  initoval  17906  termoval  17907  homafval  17942  arwval  17956  coafval  17977  coapm  17984  setccatid  17997  catchomfval  18015  catccofval  18017  catccatid  18019  elestrchom  18040  estrccatid  18044  xpcbas  18090  xpchomfval  18091  xpccofval  18094  1stf1  18104  1stf2  18105  2ndf1  18107  2ndf2  18108  prf1  18112  prf2fval  18113  evlf2  18130  evlf1  18132  curf1fval  18136  curf11  18138  curf12  18139  curf1cl  18140  curf2  18141  curf2cl  18143  hof2fval  18167  yonedalem4a  18187  yonedalem4c  18189  yonedalem3  18192  yonedainv  18193  oduprs  18212  isdrs  18213  ispos  18226  odupos  18238  pltfval  18241  lubfval  18260  lubeldm  18263  lubval  18266  glbfval  18273  glbeldm  18276  glbval  18279  odulub  18317  odujoin  18318  oduglb  18319  odumeet  18320  clatlem  18414  clatlubcl2  18416  clatglbcl2  18418  isdlat  18434  ipolt  18447  ipopos  18448  isacs4lem  18456  plusffval  18560  issstrmgm  18567  gsumvalx  18590  gsumval  18591  ismgmhm  18610  issubmgm2  18617  submgmacs  18631  issubmnd  18675  ress0g  18676  ismhm  18699  mndvcl  18711  0subm  18731  0mhm  18733  submacs  18741  pwsdiagmhm  18745  gsumz  18750  frmdplusg  18768  efmndplusg  18794  efmndmgm  18799  smndex1mgm  18821  grpinvfval  18897  grpsubfval  18902  grpsubfvalALT  18903  mulgfval  18988  mulgfvalALT  18989  mulgval  18990  issubg  19045  0subg  19070  subgacs  19079  nsgacs  19080  nmznsg  19086  eqgfval  19094  isghm  19133  isghmOLD  19134  gicen  19196  isga  19209  subgga  19218  orbstafun  19229  orbstaval  19230  orbsta  19231  cntzfval  19238  cntzval  19239  oppgplusfval  19266  oppglt  19286  symg2bas  19311  symgvalstruct  19315  cayleylem2  19331  psgnfval  19418  odfval  19450  odinf  19481  dfod2  19482  0subgALT  19486  pgpfi1  19513  pgp0  19514  sylow1lem2  19517  sylow3lem6  19550  lsmfval  19556  lsmvalx  19557  oppglsm  19560  pj1fval  19612  efglem  19634  efgrelexlemb  19668  efgcpbllemb  19673  frgpeccl  19679  frgpmhm  19683  vrgpval  19685  frgpuplem  19690  frgpupf  19691  frgpupval  19692  frgpup1  19693  frgpup3lem  19695  frgpnabllem2  19792  iscygodd  19806  prmcyg  19812  lt6abl  19813  gsumval3a  19821  gsumval3  19825  gsumzres  19827  gsumzcl2  19828  gsumzf1o  19830  gsumreidx  19835  gsumzaddlem  19839  gsumzadd  19840  gsumzsplit  19845  gsummptshft  19854  gsumzmhm  19855  gsumzoppg  19862  gsumzinv  19863  gsummptfidminv  19865  gsumsub  19866  gsumpt  19880  gsummptf1o  19881  gsum2dlem1  19888  gsum2dlem2  19889  gsum2d  19890  gsum2d2lem  19891  gsumxp2  19898  fsfnn0gsumfsffz  19901  nn0gsumfz  19902  gsummptnn0fz  19904  dprdfid  19937  dprdfinv  19939  dprdfadd  19940  dprdfeq0  19942  dmdprdsplitlem  19957  dpjidcl  19978  ablfacrplem  19985  ablfacrp  19986  ablfacrp2  19987  ablfac1a  19989  ablfac1b  19990  ablfac1c  19991  ablfac1eu  19993  pgpfaclem2  20002  ablfaclem2  20006  ablfaclem3  20007  2nsgsimpgd  20022  prmgrpsimpgd  20034  ablsimpgprmd  20035  mgpplusg  20068  mgpress  20074  issrg  20112  ring1ne0  20223  gsumdixp  20243  pwsmgp  20251  opprmulfval  20263  dvdsrval  20285  isunit  20297  unitgrp  20307  unitlinv  20317  unitrinv  20318  dvrfval  20326  rdivmuldivd  20337  rnghmval  20364  isrnghm  20365  c0snmgmhm  20386  c0snmhm  20387  isnzr2  20439  isnzr2hash  20440  0ring  20447  0ringdif  20448  01eq0ringOLD  20452  0ring01eqbi  20453  zrrnghm  20457  issubrg  20492  subrgugrp  20512  rngcrescrhm  20605  rrgval  20618  rrgsupp  20622  isdrng2  20664  drngmclOLD  20672  drngid2  20673  imadrhmcl  20718  subrgacs  20721  sdrgacs  20722  cntzsdrg  20723  subdrgint  20724  isabv  20732  staffval  20762  ofldlt1  20796  islmod  20803  scaffval  20819  lcomfsupp  20841  mptscmfsupp0  20866  rmodislmod  20869  lssset  20872  islss  20873  lsssn0  20887  lssacs  20906  lspfval  20912  lspval  20914  lspcl  20915  lspuni0  20949  lss0v  20956  0lmhm  20980  lmhmvsca  20985  islbs  21016  islbs3  21098  lbsextlem1  21101  lbsextlem3  21103  lbsextlem4  21104  lbsext  21106  rnglidl0  21172  rsp1  21180  2idlval  21194  qusrhm  21219  expghm  21418  zrhrhmb  21453  zlmvsca  21464  zntoslem  21499  znfi  21502  znunithash  21507  psgnghm  21523  psgnghm2  21524  psgnevpmb  21530  ipffval  21591  ocvfval  21609  ocvval  21610  elocv  21611  thlbas  21639  thlle  21640  thlleval  21641  thloc  21642  pjfval  21649  pjdm  21650  pjpm  21651  isobs  21663  frlmbas  21698  frlmbasf  21703  frlmvscafval  21709  frlmvscavalb  21713  frlmsslss2  21718  frlmip  21721  uvcvval  21729  uvcvvcl  21730  frlmssuvc2  21738  frlmsslsp  21739  ellspd  21745  elfilspd  21746  islinds2  21756  islindf4  21781  aspval  21816  psrbas  21876  psrelbas  21877  psrplusg  21879  psrmulr  21885  psrvscafval  21891  psrvscacl  21894  psr0lid  21896  psrlidm  21905  psrridm  21906  resspsradd  21918  resspsrmul  21919  resspsrvsca  21920  psrascl  21922  mvrval2  21926  mplsubglem  21942  mpllsslem  21943  mplsubrglem  21947  ressmpladd  21970  ressmplmul  21971  ressmplvsca  21972  mplmon  21976  mplmonmul  21977  mplcoe1  21978  opsrle  21988  opsrtoslem2  21997  mplmon2  22002  evlslem4  22017  psrbagev1  22018  evlslem2  22020  evlslem3  22021  evlsval2  22028  selvval  22056  mhpval  22060  ismhp3  22063  psdfval  22079  coe1sfi  22132  coe1fsupp  22133  mptcoe1fsupp  22134  coe1ae0  22135  ressply1add  22148  ressply1mul  22149  ressply1vsca  22150  gsumply1subr  22152  psropprmul  22156  coe1tmmul2fv  22198  coe1pwmulfv  22200  ply1coe  22219  cply1coe0  22222  cply1coe0bi  22223  gsummoncoe1  22229  evls1fval  22240  evls1val  22241  evls1rhmlem  22242  evls1sca  22244  evls1gsumadd  22245  evls1gsummul  22246  evl1val  22250  evl1fval1lem  22251  fveval1fvcl  22254  evl1sca  22255  evl1var  22257  evl1addd  22262  evl1subd  22263  evl1muld  22264  evl1expd  22266  pf1f  22271  pf1mpf  22273  pf1ind  22276  evl1gsummul  22281  evls1expd  22288  evls1fpws  22290  evls1addd  22292  evls1muld  22293  evls1vsca  22294  rhmply1vr1  22308  mamures  22318  mamucl  22322  mamuvs1  22326  mamuvs2  22327  matbas2d  22344  matecl  22346  mamumat1cl  22360  mat1comp  22361  mamulid  22362  mamurid  22363  mat1ov  22369  matsc  22371  mat1dimelbas  22392  mat1dimmul  22397  mat1f1o  22399  dmatval  22413  dmatmulcl  22421  scmatval  22425  scmatscmiddistr  22429  mavmulcl  22468  1mavmul  22469  marrepfval  22481  marrepeval  22484  marepvfval  22486  submafval  22500  mdetfval  22507  mdetunilem9  22541  mdetuni0  22542  m2detleiblem3  22550  m2detleiblem4  22551  minmar1fval  22567  minmar1eval  22570  symgmatr01  22575  gsummatr01lem3  22578  gsummatr01  22580  smadiadetlem1a  22584  smadiadetlem3  22589  invrvald  22597  cpmat  22630  mat2pmatfval  22644  mat2pmatbas  22647  decpmatfsupp  22690  decpmatmulsumfsupp  22694  pmatcollpw3lem  22704  pmatcollpw3fi1lem2  22708  pm2mpval  22716  mply1topmatcl  22726  chmatval  22750  chpmatfval  22751  chfacffsupp  22777  chfacfscmul0  22779  chfacfscmulfsupp  22780  chfacfpmmul0  22783  chfacfpmmulfsupp  22784  cpmidpmatlem2  22792  cpmadumatpolylem1  22802  imastopn  23641  uzrest  23818  tmdgsum2  24017  distgp  24020  indistgp  24021  snclseqg  24037  tsmsval  24052  tsms0  24063  tsmsres  24065  tsmsxplem1  24074  tsmsxplem2  24075  ussid  24181  isusp  24182  ressust  24184  cnextucn  24223  prdsxmetlem  24289  nrmmetd  24495  nmfval  24509  tngds  24569  tngnm  24572  tngngp2  24573  tngngpd  24574  tngngp  24575  tngngp3  24577  nmo0  24656  xrrest  24729  climcncf  24826  cphsubrglem  25110  cphcjcl  25116  tcphex  25150  ipcau2  25167  cmsss  25284  rrxip  25323  minveclem4a  25363  minveclem4  25365  mbflimsup  25600  mbflim  25602  mdegfval  26000  mdegleb  26002  mdegldg  26004  deg1val  26034  uc1pval  26078  mon1pval  26080  q1pval  26093  r1pval  26096  ply1remlem  26103  ply1rem  26104  fta1glem1  26106  fta1glem2  26107  fta1blem  26109  idomrootle  26111  ig1pval  26114  elqaalem3  26262  ulmcau  26337  ulmdvlem1  26342  ulmdvlem3  26344  mbfulm  26348  itgulm  26350  dchrplusg  27191  dchrmullid  27196  dchrinvcl  27197  dchrptlem2  27209  dchrptlem3  27210  dchrsum2  27212  sumdchr2  27214  dchr2sum  27217  axtgcont1  28452  tgjustc1  28459  tgjustc2  28460  tglowdim1  28484  tgldimor  28486  tgldim0eq  28487  iscgrgd  28497  isismt  28518  tglnfn  28531  tglnunirn  28532  tglngval  28535  legval  28568  ishlg  28586  hlcgrex  28600  hlcgreulem  28601  mirval  28639  midexlem  28676  israg  28681  perpln1  28694  perpln2  28695  isperp  28696  ishpg  28743  midf  28760  ismidb  28762  lmif  28769  islmib  28771  iscgra  28793  isinag  28822  isleag  28831  iseqlg  28851  ttgval  28859  ttgitvval  28866  setsvtx  29020  uhgrunop  29060  incistruhgr  29064  upgrunop  29104  umgrunop  29106  usgriedgleord  29213  uspgredgleord  29217  uhgr0vsize0  29224  lfuhgr1v0e  29239  uhgrspanop  29281  upgrspanop  29282  umgrspanop  29283  usgrspanop  29284  uhgrspan1lem1  29285  upgrres1lem1  29294  usgredgffibi  29309  fusgredgfi  29310  usgr1v0e  29311  nbgr2vtx1edg  29335  nbuhgr2vtx1edgb  29337  nbfusgrlevtxm1  29362  nbfusgrlevtxm2  29363  uvtx01vtx  29382  cplgr1vlem  29414  cplgr1v  29415  cusgrsize2inds  29439  cusgrfilem3  29443  sizusglecusg  29449  fusgrmaxsize  29450  vtxdgfval  29453  vtxdun  29467  vtxd0nedgb  29474  p1evtxdeqlem  29498  p1evtxdeq  29499  p1evtxdp1  29500  usgrvd0nedg  29519  vtxdginducedm1lem1  29525  vtxdginducedm1lem4  29528  vtxdginducedm1  29529  vtxdginducedm1fi  29530  finsumvtxdg2ssteplem4  29534  rusgrnumwrdl2  29572  wksfval  29595  iswlkg  29599  wlkonprop  29642  wlkp1lem3  29659  wlkp1lem8  29664  wlkp1  29665  wksonproplem  29688  wwlks  29820  wwlksnon  29836  wspthsnon  29837  clwwlk  29970  0wlkonlem2  30106  conngrv2edg  30182  eupthp1  30203  eupth2eucrct  30204  eupthvdres  30222  eupth2lem3  30223  eupth2lemb  30224  3cyclfrgrrn  30273  frgrwopreglem1  30299  frgrwopreg1  30305  imsmetlem  30677  dipfval  30689  sspval  30710  islno  30740  nmooval  30750  nmounbseqi  30764  nmobndseqi  30766  0ofval  30774  0oval  30775  ajfval  30796  isph  30809  phpar  30811  ajval  30848  ubthlem1  30857  ubthlem2  30858  minvecolem4b  30865  minvecolem4  30867  minvecolem5  30868  hlex  30885  fpwrelmap  32723  ressplusf  32951  ressnm  32952  ressprs  32954  ismnt  32971  mgcval  32975  gsummptres  33039  gsummptres2  33040  gsumfs2d  33042  gsumpart  33044  gsumhashmul  33048  gsumwrd2dccat  33054  conjga  33146  inftmrel  33156  isinftm  33157  gsumvsca1  33202  ress1r  33208  ringinvval  33209  dvrcan5  33210  rmfsupp2  33212  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem3  33218  elrgspnlem4  33219  elrgspn  33220  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  erlval  33232  rlocval  33233  rlocbas  33241  rlocaddval  33242  rlocmulval  33243  rlocf1  33247  fldgenval  33285  resvsca  33304  quslmod  33330  islinds5  33339  ellspds  33340  elrsp  33344  linds2eq  33353  elringlsm  33365  lsmsnpridl  33370  grplsm0l  33375  qusima  33380  nsgmgc  33384  nsgqusf1o  33388  elrspunidl  33400  elrspunsn  33401  drngidlhash  33406  prmidl0  33422  oppreqg  33455  opprqusbas  33460  qsdrngi  33467  idlsrgbas  33476  idlsrgplusg  33477  idlsrgmulr  33479  idlsrgtset  33480  rprmval  33488  1arithidom  33509  fply1  33528  evls1fvf  33532  evl1fvf  33533  coe1zfv  33558  r1pquslmic  33578  mplvrpmfgalem  33581  mplvrpmga  33582  resssra  33606  exsslsb  33616  lbslelsp  33617  dimval  33620  dimvalfi  33621  lvecdim0  33626  ply1degltdimlem  33642  irngval  33705  elirng  33706  irngss  33707  irngnzply1lem  33710  extdgfialglem2  33713  minplyval  33725  constrsuc  33758  constrelextdg2  33767  mdetpmtr1  33843  rspectopn  33887  zarcls0  33888  zarcls  33894  zartopn  33895  zarmxt1  33900  rhmpreimacnlem  33904  rhmpreimacn  33905  pstmfval  33916  ordtrest2NEW  33943  ordtconnlem1  33944  fsumcvg4  33970  pl1cn  33975  qqhval  33992  sibf0  34354  sitgclg  34362  sitgaddlemb  34368  eulerpartlemgvv  34396  afsval  34691  onvf1odlem3  35156  pthhashvtx  35179  usgrcyclgt2v  35182  cusgr3cyclex  35187  acycgr2v  35201  cusgracyclt3v  35207  mrsubfval  35559  mrsubcv  35561  mrsubff  35563  mrsubrn  35564  elmrsubrn  35571  msubfval  35575  msubff  35581  mpstval  35586  elmpst  35587  msrval  35589  mstaval  35595  msubvrs  35611  mclsssvlem  35613  mclsval  35614  mclsind  35621  mppsval  35623  climlec3  35785  sdclem2  37788  sdclem1  37789  caures  37806  heiborlem3  37859  heibor  37867  grpokerinj  37939  rngoi  37945  dvrunz  38000  isdrngo1  38002  isdrngo2  38004  isrngohom  38011  idlval  38059  isidl  38060  0idl  38071  0rngo  38073  divrngidl  38074  smprngopr  38098  igenval  38107  lshpset  39083  lsatset  39095  lcvfbr  39125  islfl  39165  lfl0f  39174  lfl1  39175  lfladd0l  39179  lflnegl  39181  lflvscl  39182  lflvsdi1  39183  lflvsdi2  39184  lflvsdi2a  39185  lflvsass  39186  lfl0sc  39187  lflsc0N  39188  lfl1sc  39189  lkr0f  39199  lkrsc  39202  eqlkr2  39205  ldualvbase  39231  ldualfvadd  39233  ldualvaddval  39236  ldualsca  39237  ldualfvs  39241  ldualvsval  39243  isopos  39285  cmtfvalN  39315  cvrfval  39373  pats  39390  llnset  39610  lplnset  39634  lvolset  39677  lineset  39843  isline  39844  pointsetN  39846  psubspset  39849  ispsubsp  39850  pmapval  39862  paddfval  39902  paddval  39903  pclfvalN  39994  pclvalN  39995  polfvalN  40009  polvalN  40010  psubclsetN  40041  ispsubclN  40042  watvalN  40098  lhpset  40100  lautset  40187  islaut  40188  pautsetN  40203  ispautN  40204  ldilset  40214  ltrnset  40223  dilsetN  40258  cdleme26e  40464  cdleme26eALTN  40466  cdleme26fALTN  40467  cdleme26f  40468  cdleme26f2ALTN  40469  cdleme26f2  40470  cdlemefs32sn1aw  40519  cdleme43fsv1snlem  40525  cdleme41sn3a  40538  cdleme32a  40546  cdleme40m  40572  cdleme40n  40573  cdleme42b  40583  tgrpbase  40851  tgrpopr  40852  istendo  40865  tendopl  40881  tendo02  40892  erngbase  40906  erngfplus  40907  erngfmul  40910  erngbase-rN  40914  erngfplus-rN  40915  erngfmul-rN  40918  cdlemk36  41018  cdlemkid  41041  dvasca  41111  dvavbase  41118  dvafvadd  41119  dvafvsca  41121  diafval  41136  diaval  41137  dvhsca  41187  dvhvbase  41192  dvhfvadd  41196  dvhfvsca  41205  docafvalN  41227  docavalN  41228  djafvalN  41239  djavalN  41240  dibfval  41246  dibopelvalN  41248  dibopelval2  41250  dibelval3  41252  diblsmopel  41276  dicfval  41280  dicval  41281  cdlemn11a  41312  dihvalcqpre  41340  dihopelvalcpre  41353  dihord6apre  41361  dihpN  41441  dochfval  41455  dochval  41456  djhfval  41502  djhval  41503  islpolN  41588  lpolconN  41592  dochpolN  41595  lcfrlem9  41655  lcd0vvalN  41718  mapdval  41733  mapd1o  41753  mapdunirnN  41755  mapdhval  41829  mapdhval0  41830  hvmapfval  41864  hvmapval  41865  hdmap1fval  41901  hdmap1vallem  41902  hgmapfval  41991  hlhilset  42039  hlhilbase  42041  hlhilplus  42042  hlhilvsca  42052  hlhilip  42053  hlhilnvl  42055  hlhillsm  42061  hlhillcs  42063  hashscontpow  42221  frlmfielbas  42599  fimgmcyc  42633  frlm0vald  42638  evlsval3  42658  evlsbagval  42665  selvcllem5  42681  evlselv  42686  fsuppind  42689  fsuppssind  42692  mhpind  42693  mhphf  42696  sn-isghm  42772  islssfgi  43170  pwssplit4  43187  frlmpwfi  43196  mendplusgfval  43279  mendmulrfval  43281  mendvscafval  43284  idomodle  43289  deg1mhm  43298  mnringelbased  44315  mnring0g2d  44320  mnringmulrd  44321  mnringmulrcld  44326  dvgrat  44410  uzmptshftfval  44444  climexp  45710  climinf  45711  climneg  45715  climdivf  45717  climconstmpt  45761  climresmpt  45762  climsubmpt  45763  fnlimfvre  45777  limsupvaluz  45811  limsupequzmpt2  45821  climuzlem  45846  climisp  45849  climxrrelem  45852  climxrre  45853  limsupgtlem  45880  liminflelimsupuz  45888  liminfgelimsupuz  45891  liminfequzmpt2  45894  liminfvaluz  45895  limsupvaluz3  45901  climliminflimsupd  45904  liminfreuzlem  45905  liminfltlem  45907  liminflimsupclim  45910  liminflbuz2  45918  liminfpnfuz  45919  xlimclim2lem  45942  climxlim2  45949  sge0isum  46530  sge0uzfsumgt  46547  sge0seq  46549  meaiunlelem  46571  caragendifcl  46617  omeiunle  46620  omeiunltfirp  46622  carageniuncl  46626  caragensal  46628  opnssborel  46738  smflimlem6  46879  smfpimcc  46911  smflimmpt  46913  smflimsuplem4  46926  smflimsuplem6  46928  smflimsuplem8  46930  smfliminflem  46933  clnbgrlevtx  47950  isisubgr  47967  isubgriedg  47968  isubgrvtx  47972  isuspgrim  48001  gricen  48030  ushggricedg  48032  uhgrimisgrgric  48036  grtri  48045  isubgr3stgrlem2  48072  grlicen  48122  clnbgr3stgrgrlim  48124  clnbgr3stgrgrlic  48125  upwlksfval  48240  isupwlkg  48242  copisnmnd  48274  zlidlring  48339  cznrng  48366  cznnring  48367  rngchomfvalALTV  48372  rngccofvalALTV  48375  rngccatidALTV  48377  rngcrescrhmALTV  48385  ringchomfvalALTV  48406  ringccofvalALTV  48409  ringccatidALTV  48411  ofaddmndmap  48448  suppmptcfin  48481  mptcfsupp  48482  dmatALTbas  48507  lcoop  48517  linccl  48520  lcosn0  48526  lincvalsc0  48527  lcoc0  48528  linc0scn0  48529  linc1  48531  lincscmcl  48538  islinindfis  48555  lincext1  48560  lincext2  48561  lindslinindimp2lem2  48565  lindslinindimp2lem3  48566  lindsrng01  48574  snlindsntorlem  48576  snlindsntor  48577  ldepspr  48579  lincresunit1  48583  lincresunit2  48584  lines  48837  line  48838  rrxlines  48839  sphere  48853  rrxsphere  48854  discsubc  49170  nelsubclem  49173  funcf2lem2  49188  cofidvala  49222  cofidval  49225  upfval  49282  upfval2  49283  isnatd  49329  swapf2fvala  49370  swapf1vala  49372  tposcurf1  49405  diag1f1lem  49412  fuco112  49435  functhinclem1  49550  thincciso  49559  oppcterm  49612  functermc2  49615  idfudiag1bas  49630  idfudiag1  49631  cmddu  49774