Theorem fvexi 6831

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

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

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 5239

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 4279  df-sn 4572  df-pr 4574  df-uni 4855  df-iota 6432  df-fv 6484

This theorem is referenced by:  mptfvmpt  7157  ovex  7374  mapfienlem1  9284  climle  15542  climsup  15572  iserabs  15717  isumshft  15741  explecnv  15767  prodfclim1  15795  ressbas  17142  ressbas2  17144  ressid  17150  ressval3d  17152  topnid  17334  prdsplusg  17357  prdsmulr  17358  prdsvsca  17359  prdsip  17360  prdsle  17361  prdsds  17363  prdshom  17366  prdsco  17367  pwselbasb  17387  pwsvscafval  17393  pwssca  17395  pwssnf1o  17397  imassca  17418  imasvsca  17419  imasle  17422  xpsrnbas  17470  xpssca  17475  xpsvsca  17476  isacs2  17554  homffval  17591  comfffval  17599  oppchomfval  17615  oppccofval  17617  oppccatid  17620  monfval  17634  oppcmon  17640  sectffval  17652  invffval  17660  rescbas  17731  reschom  17732  rescco  17734  fullsubc  17752  isfunc  17766  isfuncd  17767  idfu2nd  17779  idfu1st  17781  cofu1st  17785  cofu2nd  17787  fucco  17867  fucid  17876  invfuc  17879  initoval  17895  termoval  17896  homafval  17931  arwval  17945  coafval  17966  coapm  17973  setccatid  17986  catchomfval  18004  catccofval  18006  catccatid  18008  elestrchom  18029  estrccatid  18033  xpcbas  18079  xpchomfval  18080  xpccofval  18083  1stf1  18093  1stf2  18094  2ndf1  18096  2ndf2  18097  prf1  18101  prf2fval  18102  evlf2  18119  evlf1  18121  curf1fval  18125  curf11  18127  curf12  18128  curf1cl  18129  curf2  18130  curf2cl  18132  hof2fval  18156  yonedalem4a  18176  yonedalem4c  18178  yonedalem3  18181  yonedainv  18182  oduprs  18201  isdrs  18202  ispos  18215  odupos  18227  pltfval  18230  lubfval  18249  lubeldm  18252  lubval  18255  glbfval  18262  glbeldm  18265  glbval  18268  odulub  18306  odujoin  18307  oduglb  18308  odumeet  18309  clatlem  18403  clatlubcl2  18405  clatglbcl2  18407  isdlat  18423  ipolt  18436  ipopos  18437  isacs4lem  18445  plusffval  18549  issstrmgm  18556  gsumvalx  18579  gsumval  18580  ismgmhm  18599  issubmgm2  18606  submgmacs  18620  issubmnd  18664  ress0g  18665  ismhm  18688  mndvcl  18700  0subm  18720  0mhm  18722  submacs  18730  pwsdiagmhm  18734  gsumz  18739  frmdplusg  18757  efmndplusg  18783  efmndmgm  18788  smndex1mgm  18810  grpinvfval  18886  grpsubfval  18891  grpsubfvalALT  18892  mulgfval  18977  mulgfvalALT  18978  mulgval  18979  issubg  19034  0subg  19059  subgacs  19068  nsgacs  19069  nmznsg  19075  eqgfval  19083  isghm  19122  isghmOLD  19123  gicen  19185  isga  19198  subgga  19207  orbstafun  19218  orbstaval  19219  orbsta  19220  cntzfval  19227  cntzval  19228  oppgplusfval  19255  oppglt  19275  symg2bas  19300  symgvalstruct  19304  cayleylem2  19320  psgnfval  19407  odfval  19439  odinf  19470  dfod2  19471  0subgALT  19475  pgpfi1  19502  pgp0  19503  sylow1lem2  19506  sylow3lem6  19539  lsmfval  19545  lsmvalx  19546  oppglsm  19549  pj1fval  19601  efglem  19623  efgrelexlemb  19657  efgcpbllemb  19662  frgpeccl  19668  frgpmhm  19672  vrgpval  19674  frgpuplem  19679  frgpupf  19680  frgpupval  19681  frgpup1  19682  frgpup3lem  19684  frgpnabllem2  19781  iscygodd  19795  prmcyg  19801  lt6abl  19802  gsumval3a  19810  gsumval3  19814  gsumzres  19816  gsumzcl2  19817  gsumzf1o  19819  gsumreidx  19824  gsumzaddlem  19828  gsumzadd  19829  gsumzsplit  19834  gsummptshft  19843  gsumzmhm  19844  gsumzoppg  19851  gsumzinv  19852  gsummptfidminv  19854  gsumsub  19855  gsumpt  19869  gsummptf1o  19870  gsum2dlem1  19877  gsum2dlem2  19878  gsum2d  19879  gsum2d2lem  19880  gsumxp2  19887  fsfnn0gsumfsffz  19890  nn0gsumfz  19891  gsummptnn0fz  19893  dprdfid  19926  dprdfinv  19928  dprdfadd  19929  dprdfeq0  19931  dmdprdsplitlem  19946  dpjidcl  19967  ablfacrplem  19974  ablfacrp  19975  ablfacrp2  19976  ablfac1a  19978  ablfac1b  19979  ablfac1c  19980  ablfac1eu  19982  pgpfaclem2  19991  ablfaclem2  19995  ablfaclem3  19996  2nsgsimpgd  20011  prmgrpsimpgd  20023  ablsimpgprmd  20024  mgpplusg  20057  mgpress  20063  issrg  20101  ring1ne0  20212  gsumdixp  20232  pwsmgp  20240  opprmulfval  20252  dvdsrval  20274  isunit  20286  unitgrp  20296  unitlinv  20306  unitrinv  20307  dvrfval  20315  rdivmuldivd  20326  rnghmval  20353  isrnghm  20354  c0snmgmhm  20375  c0snmhm  20376  isnzr2  20428  isnzr2hash  20429  0ring  20436  0ringdif  20437  01eq0ringOLD  20441  0ring01eqbi  20442  zrrnghm  20446  issubrg  20481  subrgugrp  20501  rngcrescrhm  20594  rrgval  20607  rrgsupp  20611  isdrng2  20653  drngmclOLD  20661  drngid2  20662  imadrhmcl  20707  subrgacs  20710  sdrgacs  20711  cntzsdrg  20712  subdrgint  20713  isabv  20721  staffval  20751  ofldlt1  20785  islmod  20792  scaffval  20808  lcomfsupp  20830  mptscmfsupp0  20855  rmodislmod  20858  lssset  20861  islss  20862  lsssn0  20876  lssacs  20895  lspfval  20901  lspval  20903  lspcl  20904  lspuni0  20938  lss0v  20945  0lmhm  20969  lmhmvsca  20974  islbs  21005  islbs3  21087  lbsextlem1  21090  lbsextlem3  21092  lbsextlem4  21093  lbsext  21095  rnglidl0  21161  rsp1  21169  2idlval  21183  qusrhm  21208  expghm  21407  zrhrhmb  21442  zlmvsca  21453  zntoslem  21488  znfi  21491  znunithash  21496  psgnghm  21512  psgnghm2  21513  psgnevpmb  21519  ipffval  21580  ocvfval  21598  ocvval  21599  elocv  21600  thlbas  21628  thlle  21629  thlleval  21630  thloc  21631  pjfval  21638  pjdm  21639  pjpm  21640  isobs  21652  frlmbas  21687  frlmbasf  21692  frlmvscafval  21698  frlmvscavalb  21702  frlmsslss2  21707  frlmip  21710  uvcvval  21718  uvcvvcl  21719  frlmssuvc2  21727  frlmsslsp  21728  ellspd  21734  elfilspd  21735  islinds2  21745  islindf4  21770  aspval  21805  psrbas  21865  psrelbas  21866  psrplusg  21868  psrmulr  21874  psrvscafval  21880  psrvscacl  21883  psr0lid  21885  psrlidm  21894  psrridm  21895  resspsradd  21907  resspsrmul  21908  resspsrvsca  21909  psrascl  21911  mvrval2  21915  mplsubglem  21931  mpllsslem  21932  mplsubrglem  21936  ressmpladd  21959  ressmplmul  21960  ressmplvsca  21961  mplmon  21965  mplmonmul  21966  mplcoe1  21967  opsrle  21977  opsrtoslem2  21986  mplmon2  21991  evlslem4  22006  psrbagev1  22007  evlslem2  22009  evlslem3  22010  evlsval2  22017  selvval  22045  mhpval  22049  ismhp3  22052  psdfval  22068  coe1sfi  22121  coe1fsupp  22122  mptcoe1fsupp  22123  coe1ae0  22124  ressply1add  22137  ressply1mul  22138  ressply1vsca  22139  gsumply1subr  22141  psropprmul  22145  coe1tmmul2fv  22187  coe1pwmulfv  22189  ply1coe  22208  cply1coe0  22211  cply1coe0bi  22212  gsummoncoe1  22218  evls1fval  22229  evls1val  22230  evls1rhmlem  22231  evls1sca  22233  evls1gsumadd  22234  evls1gsummul  22235  evl1val  22239  evl1fval1lem  22240  fveval1fvcl  22243  evl1sca  22244  evl1var  22246  evl1addd  22251  evl1subd  22252  evl1muld  22253  evl1expd  22255  pf1f  22260  pf1mpf  22262  pf1ind  22265  evl1gsummul  22270  evls1expd  22277  evls1fpws  22279  evls1addd  22281  evls1muld  22282  evls1vsca  22283  rhmply1vr1  22297  mamures  22307  mamucl  22311  mamuvs1  22315  mamuvs2  22316  matbas2d  22333  matecl  22335  mamumat1cl  22349  mat1comp  22350  mamulid  22351  mamurid  22352  mat1ov  22358  matsc  22360  mat1dimelbas  22381  mat1dimmul  22386  mat1f1o  22388  dmatval  22402  dmatmulcl  22410  scmatval  22414  scmatscmiddistr  22418  mavmulcl  22457  1mavmul  22458  marrepfval  22470  marrepeval  22473  marepvfval  22475  submafval  22489  mdetfval  22496  mdetunilem9  22530  mdetuni0  22531  m2detleiblem3  22539  m2detleiblem4  22540  minmar1fval  22556  minmar1eval  22559  symgmatr01  22564  gsummatr01lem3  22567  gsummatr01  22569  smadiadetlem1a  22573  smadiadetlem3  22578  invrvald  22586  cpmat  22619  mat2pmatfval  22633  mat2pmatbas  22636  decpmatfsupp  22679  decpmatmulsumfsupp  22683  pmatcollpw3lem  22693  pmatcollpw3fi1lem2  22697  pm2mpval  22705  mply1topmatcl  22715  chmatval  22739  chpmatfval  22740  chfacffsupp  22766  chfacfscmul0  22768  chfacfscmulfsupp  22769  chfacfpmmul0  22772  chfacfpmmulfsupp  22773  cpmidpmatlem2  22781  cpmadumatpolylem1  22791  imastopn  23630  uzrest  23807  tmdgsum2  24006  distgp  24009  indistgp  24010  snclseqg  24026  tsmsval  24041  tsms0  24052  tsmsres  24054  tsmsxplem1  24063  tsmsxplem2  24064  ussid  24170  isusp  24171  ressust  24173  cnextucn  24212  prdsxmetlem  24278  nrmmetd  24484  nmfval  24498  tngds  24558  tngnm  24561  tngngp2  24562  tngngpd  24563  tngngp  24564  tngngp3  24566  nmo0  24645  xrrest  24718  climcncf  24815  cphsubrglem  25099  cphcjcl  25105  tcphex  25139  ipcau2  25156  cmsss  25273  rrxip  25312  minveclem4a  25352  minveclem4  25354  mbflimsup  25589  mbflim  25591  mdegfval  25989  mdegleb  25991  mdegldg  25993  deg1val  26023  uc1pval  26067  mon1pval  26069  q1pval  26082  r1pval  26085  ply1remlem  26092  ply1rem  26093  fta1glem1  26095  fta1glem2  26096  fta1blem  26098  idomrootle  26100  ig1pval  26103  elqaalem3  26251  ulmcau  26326  ulmdvlem1  26331  ulmdvlem3  26333  mbfulm  26337  itgulm  26339  dchrplusg  27180  dchrmullid  27185  dchrinvcl  27186  dchrptlem2  27198  dchrptlem3  27199  dchrsum2  27201  sumdchr2  27203  dchr2sum  27206  axtgcont1  28441  tgjustc1  28448  tgjustc2  28449  tglowdim1  28473  tgldimor  28475  tgldim0eq  28476  iscgrgd  28486  isismt  28507  tglnfn  28520  tglnunirn  28521  tglngval  28524  legval  28557  ishlg  28575  hlcgrex  28589  hlcgreulem  28590  mirval  28628  midexlem  28665  israg  28670  perpln1  28683  perpln2  28684  isperp  28685  ishpg  28732  midf  28749  ismidb  28751  lmif  28758  islmib  28760  iscgra  28782  isinag  28811  isleag  28820  iseqlg  28840  ttgval  28848  ttgitvval  28855  setsvtx  29008  uhgrunop  29048  incistruhgr  29052  upgrunop  29092  umgrunop  29094  usgriedgleord  29201  uspgredgleord  29205  uhgr0vsize0  29212  lfuhgr1v0e  29227  uhgrspanop  29269  upgrspanop  29270  umgrspanop  29271  usgrspanop  29272  uhgrspan1lem1  29273  upgrres1lem1  29282  usgredgffibi  29297  fusgredgfi  29298  usgr1v0e  29299  nbgr2vtx1edg  29323  nbuhgr2vtx1edgb  29325  nbfusgrlevtxm1  29350  nbfusgrlevtxm2  29351  uvtx01vtx  29370  cplgr1vlem  29402  cplgr1v  29403  cusgrsize2inds  29427  cusgrfilem3  29431  sizusglecusg  29437  fusgrmaxsize  29438  vtxdgfval  29441  vtxdun  29455  vtxd0nedgb  29462  p1evtxdeqlem  29486  p1evtxdeq  29487  p1evtxdp1  29488  usgrvd0nedg  29507  vtxdginducedm1lem1  29513  vtxdginducedm1lem4  29516  vtxdginducedm1  29517  vtxdginducedm1fi  29518  finsumvtxdg2ssteplem4  29522  rusgrnumwrdl2  29560  wksfval  29583  iswlkg  29587  wlkonprop  29630  wlkp1lem3  29647  wlkp1lem8  29652  wlkp1  29653  wksonproplem  29676  wwlks  29808  wwlksnon  29824  wspthsnon  29825  clwwlk  29955  0wlkonlem2  30091  conngrv2edg  30167  eupthp1  30188  eupth2eucrct  30189  eupthvdres  30207  eupth2lem3  30208  eupth2lemb  30209  3cyclfrgrrn  30258  frgrwopreglem1  30284  frgrwopreg1  30290  imsmetlem  30662  dipfval  30674  sspval  30695  islno  30725  nmooval  30735  nmounbseqi  30749  nmobndseqi  30751  0ofval  30759  0oval  30760  ajfval  30781  isph  30794  phpar  30796  ajval  30833  ubthlem1  30842  ubthlem2  30843  minvecolem4b  30850  minvecolem4  30852  minvecolem5  30853  hlex  30870  ressplusf  32936  ressnm  32937  ressprs  32939  ismnt  32956  mgcval  32960  gsummptres  33024  gsummptres2  33025  gsumfs2d  33027  gsumpart  33029  gsumhashmul  33033  gsumwrd2dccat  33039  conjga  33131  inftmrel  33141  isinftm  33142  gsumvsca1  33187  ress1r  33193  ringinvval  33194  dvrcan5  33195  rmfsupp2  33197  elrgspnlem1  33201  elrgspnlem2  33202  elrgspnlem3  33203  elrgspnlem4  33204  elrgspn  33205  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  erlval  33217  rlocval  33218  rlocbas  33226  rlocaddval  33227  rlocmulval  33228  rlocf1  33232  fldgenval  33270  resvsca  33289  quslmod  33315  islinds5  33324  ellspds  33325  elrsp  33329  linds2eq  33338  elringlsm  33350  lsmsnpridl  33355  grplsm0l  33360  qusima  33365  nsgmgc  33369  nsgqusf1o  33373  elrspunidl  33385  elrspunsn  33386  drngidlhash  33391  prmidl0  33407  oppreqg  33440  opprqusbas  33445  qsdrngi  33452  idlsrgbas  33461  idlsrgplusg  33462  idlsrgmulr  33464  idlsrgtset  33465  rprmval  33473  1arithidom  33494  fply1  33513  evls1fvf  33517  evl1fvf  33518  coe1zfv  33543  r1pquslmic  33563  mplvrpmfgalem  33566  mplvrpmga  33567  resssra  33591  exsslsb  33601  lbslelsp  33602  dimval  33605  dimvalfi  33606  lvecdim0  33611  ply1degltdimlem  33627  irngval  33690  elirng  33691  irngss  33692  irngnzply1lem  33695  extdgfialglem2  33698  minplyval  33710  constrsuc  33743  constrelextdg2  33752  mdetpmtr1  33828  rspectopn  33872  zarcls0  33873  zarcls  33879  zartopn  33880  zarmxt1  33885  rhmpreimacnlem  33889  rhmpreimacn  33890  pstmfval  33901  ordtrest2NEW  33928  ordtconnlem1  33929  fsumcvg4  33955  pl1cn  33960  qqhval  33977  sibf0  34339  sitgclg  34347  sitgaddlemb  34353  eulerpartlemgvv  34381  afsval  34676  onvf1odlem3  35141  pthhashvtx  35164  usgrcyclgt2v  35167  cusgr3cyclex  35172  acycgr2v  35186  cusgracyclt3v  35192  mrsubfval  35544  mrsubcv  35546  mrsubff  35548  mrsubrn  35549  elmrsubrn  35556  msubfval  35560  msubff  35566  mpstval  35571  elmpst  35572  msrval  35574  mstaval  35580  msubvrs  35596  mclsssvlem  35598  mclsval  35599  mclsind  35606  mppsval  35608  climlec3  35770  sdclem2  37782  sdclem1  37783  caures  37800  heiborlem3  37853  heibor  37861  grpokerinj  37933  rngoi  37939  dvrunz  37994  isdrngo1  37996  isdrngo2  37998  isrngohom  38005  idlval  38053  isidl  38054  0idl  38065  0rngo  38067  divrngidl  38068  smprngopr  38092  igenval  38101  lshpset  39017  lsatset  39029  lcvfbr  39059  islfl  39099  lfl0f  39108  lfl1  39109  lfladd0l  39113  lflnegl  39115  lflvscl  39116  lflvsdi1  39117  lflvsdi2  39118  lflvsdi2a  39119  lflvsass  39120  lfl0sc  39121  lflsc0N  39122  lfl1sc  39123  lkr0f  39133  lkrsc  39136  eqlkr2  39139  ldualvbase  39165  ldualfvadd  39167  ldualvaddval  39170  ldualsca  39171  ldualfvs  39175  ldualvsval  39177  isopos  39219  cmtfvalN  39249  cvrfval  39307  pats  39324  llnset  39544  lplnset  39568  lvolset  39611  lineset  39777  isline  39778  pointsetN  39780  psubspset  39783  ispsubsp  39784  pmapval  39796  paddfval  39836  paddval  39837  pclfvalN  39928  pclvalN  39929  polfvalN  39943  polvalN  39944  psubclsetN  39975  ispsubclN  39976  watvalN  40032  lhpset  40034  lautset  40121  islaut  40122  pautsetN  40137  ispautN  40138  ldilset  40148  ltrnset  40157  dilsetN  40192  cdleme26e  40398  cdleme26eALTN  40400  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdlemefs32sn1aw  40453  cdleme43fsv1snlem  40459  cdleme41sn3a  40472  cdleme32a  40480  cdleme40m  40506  cdleme40n  40507  cdleme42b  40517  tgrpbase  40785  tgrpopr  40786  istendo  40799  tendopl  40815  tendo02  40826  erngbase  40840  erngfplus  40841  erngfmul  40844  erngbase-rN  40848  erngfplus-rN  40849  erngfmul-rN  40852  cdlemk36  40952  cdlemkid  40975  dvasca  41045  dvavbase  41052  dvafvadd  41053  dvafvsca  41055  diafval  41070  diaval  41071  dvhsca  41121  dvhvbase  41126  dvhfvadd  41130  dvhfvsca  41139  docafvalN  41161  docavalN  41162  djafvalN  41173  djavalN  41174  dibfval  41180  dibopelvalN  41182  dibopelval2  41184  dibelval3  41186  diblsmopel  41210  dicfval  41214  dicval  41215  cdlemn11a  41246  dihvalcqpre  41274  dihopelvalcpre  41287  dihord6apre  41295  dihpN  41375  dochfval  41389  dochval  41390  djhfval  41436  djhval  41437  islpolN  41522  lpolconN  41526  dochpolN  41529  lcfrlem9  41589  lcd0vvalN  41652  mapdval  41667  mapd1o  41687  mapdunirnN  41689  mapdhval  41763  mapdhval0  41764  hvmapfval  41798  hvmapval  41799  hdmap1fval  41835  hdmap1vallem  41836  hgmapfval  41925  hlhilset  41973  hlhilbase  41975  hlhilplus  41976  hlhilvsca  41986  hlhilip  41987  hlhilnvl  41989  hlhillsm  41995  hlhillcs  41997  hashscontpow  42155  frlmfielbas  42533  fimgmcyc  42567  frlm0vald  42572  evlsval3  42592  evlsbagval  42599  selvcllem5  42615  evlselv  42620  fsuppind  42623  fsuppssind  42626  mhpind  42627  mhphf  42630  sn-isghm  42706  islssfgi  43105  pwssplit4  43122  frlmpwfi  43131  mendplusgfval  43214  mendmulrfval  43216  mendvscafval  43219  idomodle  43224  deg1mhm  43233  mnringelbased  44250  mnring0g2d  44255  mnringmulrd  44256  mnringmulrcld  44261  dvgrat  44345  uzmptshftfval  44379  climexp  45645  climinf  45646  climneg  45650  climdivf  45652  climconstmpt  45696  climresmpt  45697  climsubmpt  45698  fnlimfvre  45712  limsupvaluz  45746  limsupequzmpt2  45756  climuzlem  45781  climisp  45784  climxrrelem  45787  climxrre  45788  limsupgtlem  45815  liminflelimsupuz  45823  liminfgelimsupuz  45826  liminfequzmpt2  45829  liminfvaluz  45830  limsupvaluz3  45836  climliminflimsupd  45839  liminfreuzlem  45840  liminfltlem  45842  liminflimsupclim  45845  liminflbuz2  45853  liminfpnfuz  45854  xlimclim2lem  45877  climxlim2  45884  sge0isum  46465  sge0uzfsumgt  46482  sge0seq  46484  meaiunlelem  46506  caragendifcl  46552  omeiunle  46555  omeiunltfirp  46557  carageniuncl  46561  caragensal  46563  opnssborel  46673  smflimlem6  46814  smfpimcc  46846  smflimmpt  46848  smflimsuplem4  46861  smflimsuplem6  46863  smflimsuplem8  46865  smfliminflem  46868  clnbgrlevtx  47876  isisubgr  47893  isubgriedg  47894  isubgrvtx  47898  isuspgrim  47927  gricen  47956  ushggricedg  47958  uhgrimisgrgric  47962  grtri  47971  isubgr3stgrlem2  47998  grlicen  48048  clnbgr3stgrgrlim  48050  clnbgr3stgrgrlic  48051  upwlksfval  48166  isupwlkg  48168  copisnmnd  48200  zlidlring  48265  cznrng  48292  cznnring  48293  rngchomfvalALTV  48298  rngccofvalALTV  48301  rngccatidALTV  48303  rngcrescrhmALTV  48311  ringchomfvalALTV  48332  ringccofvalALTV  48335  ringccatidALTV  48337  ofaddmndmap  48374  suppmptcfin  48407  mptcfsupp  48408  dmatALTbas  48433  lcoop  48443  linccl  48446  lcosn0  48452  lincvalsc0  48453  lcoc0  48454  linc0scn0  48455  linc1  48457  lincscmcl  48464  islinindfis  48481  lincext1  48486  lincext2  48487  lindslinindimp2lem2  48491  lindslinindimp2lem3  48492  lindsrng01  48500  snlindsntorlem  48502  snlindsntor  48503  ldepspr  48505  lincresunit1  48509  lincresunit2  48510  lines  48763  line  48764  rrxlines  48765  sphere  48779  rrxsphere  48780  discsubc  49096  nelsubclem  49099  funcf2lem2  49114  cofidvala  49148  cofidval  49151  upfval  49208  upfval2  49209  isnatd  49255  swapf2fvala  49296  swapf1vala  49298  tposcurf1  49331  diag1f1lem  49338  fuco112  49361  functhinclem1  49476  thincciso  49485  oppcterm  49538  functermc2  49541  idfudiag1bas  49556  idfudiag1  49557  cmddu  49700