MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvexi Structured version   Visualization version   GIF version

Theorem fvexi 6852
Description: The value of a class exists. Inference form of fvex 6851. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypothesis
Ref Expression
fvexi.1 𝐴 = (𝐹𝐵)
Assertion
Ref Expression
fvexi 𝐴 ∈ V

Proof of Theorem fvexi
StepHypRef Expression
1 fvexi.1 . 2 𝐴 = (𝐹𝐵)
2 fvex 6851 . 2 (𝐹𝐵) ∈ V
31, 2eqeltri 2835 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  Vcvv 3444  cfv 6492
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 2709  ax-nul 5262
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 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-sn 4586  df-pr 4588  df-uni 4865  df-iota 6444  df-fv 6500
This theorem is referenced by:  mptfvmpt  7173  ovex  7383  mapfienlem1  9275  climle  15457  climsup  15489  iserabs  15635  isumshft  15659  explecnv  15685  prodfclim1  15713  ressbas  17053  ressbasOLD  17054  ressbas2  17055  ressid  17060  ressval3d  17062  ressval3dOLD  17063  topnid  17252  prdsplusg  17275  prdsmulr  17276  prdsvsca  17277  prdsip  17278  prdsle  17279  prdsds  17281  prdshom  17284  prdsco  17285  pwselbasb  17305  pwsvscafval  17311  pwssca  17313  pwssnf1o  17315  imassca  17336  imasvsca  17337  imasle  17340  xpsrnbas  17388  xpssca  17393  xpsvsca  17394  isacs2  17468  homffval  17505  comfffval  17513  oppchomfval  17529  oppchomfvalOLD  17530  oppccofval  17532  oppccatid  17536  monfval  17550  oppcmon  17556  sectffval  17568  invffval  17576  rescbas  17647  rescbasOLD  17648  reschom  17649  rescco  17651  resccoOLD  17652  fullsubc  17671  isfunc  17685  isfuncd  17686  idfu2nd  17698  idfu1st  17700  cofu1st  17704  cofu2nd  17706  fucco  17786  fucid  17795  invfuc  17798  initoval  17814  termoval  17815  homafval  17850  arwval  17864  coafval  17885  coapm  17892  setccatid  17905  catchomfval  17923  catccofval  17925  catccatid  17927  elestrchom  17950  estrccatid  17954  xpcbas  18001  xpchomfval  18002  xpccofval  18005  1stf1  18015  1stf2  18016  2ndf1  18018  2ndf2  18019  prf1  18023  prf2fval  18024  evlf2  18042  evlf1  18044  curf1fval  18048  curf11  18050  curf12  18051  curf1cl  18052  curf2  18053  curf2cl  18055  hof2fval  18079  yonedalem4a  18099  yonedalem4c  18101  yonedalem3  18104  yonedainv  18105  isdrs  18125  ispos  18138  odupos  18152  pltfval  18155  lubfval  18174  lubeldm  18177  lubval  18180  glbfval  18187  glbeldm  18190  glbval  18193  odulub  18231  odujoin  18232  oduglb  18233  odumeet  18234  clatlem  18326  clatlubcl2  18328  clatglbcl2  18330  isdlat  18346  ipolt  18359  ipopos  18360  isacs4lem  18368  plusffval  18438  issstrmgm  18443  gsumvalx  18466  gsumval  18467  issubmnd  18518  ress0g  18519  ismhm  18538  0subm  18563  0mhm  18565  submacs  18572  pwsdiagmhm  18576  gsumz  18581  frmdplusg  18599  efmndplusg  18625  efmndmgm  18630  smndex1mgm  18652  grpinvfval  18724  grpsubfval  18729  grpsubfvalALT  18730  mulgfval  18808  mulgfvalALT  18809  mulgval  18810  issubg  18861  0subg  18886  0subgOLD  18887  subgacs  18896  nsgacs  18897  nmznsg  18903  eqgfval  18911  isghm  18941  gicen  19000  isga  19004  subgga  19013  orbstafun  19024  orbstaval  19025  orbsta  19026  cntzfval  19033  cntzval  19034  oppgplusfval  19059  symg2bas  19107  symgvalstruct  19111  symgvalstructOLD  19112  cayleylem2  19128  psgnfval  19215  odfval  19247  odinf  19277  dfod2  19278  pgpfi1  19307  pgp0  19308  sylow1lem2  19311  sylow3lem6  19344  lsmfval  19350  lsmvalx  19351  oppglsm  19354  pj1fval  19406  efglem  19428  efgrelexlemb  19462  efgcpbllemb  19467  frgpeccl  19473  frgpmhm  19477  vrgpval  19479  frgpuplem  19484  frgpupf  19485  frgpupval  19486  frgpup1  19487  frgpup3lem  19489  frgpnabllem2  19582  iscygodd  19595  prmcyg  19601  lt6abl  19602  gsumval3a  19610  gsumval3  19614  gsumzres  19616  gsumzcl2  19617  gsumzf1o  19619  gsumreidx  19624  gsumzaddlem  19628  gsumzadd  19629  gsumzsplit  19634  gsummptshft  19643  gsumzmhm  19644  gsumzoppg  19651  gsumzinv  19652  gsummptfidminv  19654  gsumsub  19655  gsumpt  19669  gsummptf1o  19670  gsum2dlem1  19677  gsum2dlem2  19678  gsum2d  19679  gsum2d2lem  19680  gsumxp2  19687  fsfnn0gsumfsffz  19690  nn0gsumfz  19691  gsummptnn0fz  19693  dprdfid  19726  dprdfinv  19728  dprdfadd  19729  dprdfeq0  19731  dmdprdsplitlem  19746  dpjidcl  19767  ablfacrplem  19774  ablfacrp  19775  ablfacrp2  19776  ablfac1a  19778  ablfac1b  19779  ablfac1c  19780  ablfac1eu  19782  pgpfaclem2  19791  ablfaclem2  19795  ablfaclem3  19796  2nsgsimpgd  19811  prmgrpsimpgd  19823  ablsimpgprmd  19824  mgpplusg  19830  mgpress  19841  mgpressOLD  19842  issrg  19849  ring1ne0  19939  gsumdixp  19957  pwsmgp  19966  opprmulfval  19975  dvdsrval  19998  isunit  20010  unitgrp  20020  unitlinv  20030  unitrinv  20031  dvrfval  20037  isdrng2  20122  drngmcl  20125  drngid2  20128  issubrg  20146  subrgugrp  20165  subrgacs  20191  sdrgacs  20192  cntzsdrg  20193  subdrgint  20194  isabv  20202  staffval  20230  islmod  20250  scaffval  20264  lcomfsupp  20286  mptscmfsupp0  20311  rmodislmod  20314  rmodislmodOLD  20315  lssset  20318  islss  20319  lsssn0  20332  lssacs  20352  lspfval  20358  lspval  20360  lspcl  20361  lspuni0  20395  lss0v  20401  0lmhm  20425  lmhmvsca  20430  islbs  20461  islbs3  20540  lbsextlem1  20543  lbsextlem3  20545  lbsextlem4  20546  lbsext  20548  rsp1  20618  2idlval  20627  qusrhm  20631  isnzr2  20657  isnzr2hash  20658  0ring  20664  01eq0ring  20666  0ring01eqbi  20667  rrgval  20681  rrgsupp  20685  expghm  20820  zrhrhmb  20835  zlmvsca  20850  zntoslem  20887  znfi  20890  znunithash  20895  psgnghm  20908  psgnghm2  20909  psgnevpmb  20915  ipffval  20976  ocvfval  20994  ocvval  20995  elocv  20996  thlbas  21024  thlbasOLD  21025  thlle  21026  thlleOLD  21027  thlleval  21028  thloc  21029  pjfval  21036  pjdm  21037  pjpm  21038  isobs  21050  frlmbas  21085  frlmbasf  21090  frlmvscafval  21096  frlmvscavalb  21100  frlmsslss2  21105  frlmip  21108  uvcvval  21116  uvcvvcl  21117  frlmssuvc2  21125  frlmsslsp  21126  ellspd  21132  elfilspd  21133  islinds2  21143  islindf4  21168  aspval  21200  psrbas  21270  psrelbas  21271  psrplusg  21273  psrmulr  21276  psrvscafval  21282  psrvscacl  21285  psr0lid  21287  psrlidm  21295  psrridm  21296  resspsradd  21308  resspsrmul  21309  resspsrvsca  21310  mvrval2  21314  mplsubglem  21328  mpllsslem  21329  mplsubrglem  21333  mpladd  21336  mplmul  21338  ressmpladd  21353  ressmplmul  21354  ressmplvsca  21355  mplmon  21359  mplmonmul  21360  mplcoe1  21361  opsrle  21371  opsrtoslem2  21386  mplmon2  21392  evlslem4  21407  psrbagev1  21408  psrbagev1OLD  21409  evlslem2  21412  evlslem3  21413  evlsval2  21420  selvval  21451  mhpval  21453  ismhp3  21456  coe1sfi  21507  coe1fsupp  21508  mptcoe1fsupp  21509  coe1ae0  21510  ressply1add  21524  ressply1mul  21525  ressply1vsca  21526  gsumply1subr  21528  psropprmul  21532  coe1tmmul2fv  21572  coe1pwmulfv  21574  ply1coe  21590  cply1coe0  21593  cply1coe0bi  21594  gsummoncoe1  21598  evls1fval  21608  evls1val  21609  evls1rhmlem  21610  evls1sca  21612  evls1gsumadd  21613  evls1gsummul  21614  evl1val  21618  evl1fval1lem  21619  fveval1fvcl  21622  evl1sca  21623  evl1var  21625  evl1addd  21630  evl1subd  21631  evl1muld  21632  evl1expd  21634  pf1f  21639  pf1mpf  21641  pf1ind  21644  evl1gsummul  21649  mamures  21662  mndvcl  21663  mamucl  21671  mamuvs1  21675  mamuvs2  21676  matbas2d  21695  matecl  21697  mamumat1cl  21711  mat1comp  21712  mamulid  21713  mamurid  21714  mat1ov  21720  matsc  21722  mat1dimelbas  21743  mat1dimmul  21748  mat1f1o  21750  dmatval  21764  dmatmulcl  21772  scmatval  21776  scmatscmiddistr  21780  mavmulcl  21819  1mavmul  21820  marrepfval  21832  marrepeval  21835  marepvfval  21837  submafval  21851  mdetfval  21858  mdetunilem9  21892  mdetuni0  21893  m2detleiblem3  21901  m2detleiblem4  21902  minmar1fval  21918  minmar1eval  21921  symgmatr01  21926  gsummatr01lem3  21929  gsummatr01  21931  smadiadetlem1a  21935  smadiadetlem3  21940  invrvald  21948  cpmat  21981  mat2pmatfval  21995  mat2pmatbas  21998  decpmatfsupp  22041  decpmatmulsumfsupp  22045  pmatcollpw3lem  22055  pmatcollpw3fi1lem2  22059  pm2mpval  22067  mply1topmatcl  22077  chmatval  22101  chpmatfval  22102  chfacffsupp  22128  chfacfscmul0  22130  chfacfscmulfsupp  22131  chfacfpmmul0  22134  chfacfpmmulfsupp  22135  cpmidpmatlem2  22143  cpmadumatpolylem1  22153  imastopn  22994  uzrest  23171  tmdgsum2  23370  distgp  23373  indistgp  23374  snclseqg  23390  tsmsval  23405  tsms0  23416  tsmsres  23418  tsmsxplem1  23427  tsmsxplem2  23428  ussid  23535  isusp  23536  ressust  23538  cnextucn  23578  prdsxmetlem  23644  nrmmetd  23853  nmfval  23867  tngds  23934  tngdsOLD  23935  tngnm  23938  tngngp2  23939  tngngpd  23940  tngngp  23941  tngngp3  23943  nmo0  24022  xrrest  24093  climcncf  24186  cphsubrglem  24464  cphcjcl  24470  tcphex  24504  ipcau2  24521  cmsss  24638  rrxip  24677  minveclem4a  24717  minveclem4  24719  mbflimsup  24953  mbflim  24955  mdegfval  25350  mdegleb  25352  mdegldg  25354  deg1val  25384  uc1pval  25427  mon1pval  25429  q1pval  25441  r1pval  25444  ply1remlem  25450  ply1rem  25451  fta1glem1  25453  fta1glem2  25454  fta1blem  25456  ig1pval  25460  elqaalem3  25604  ulmcau  25677  ulmdvlem1  25682  ulmdvlem3  25684  mbfulm  25688  itgulm  25690  dchrplusg  26518  dchrmulid2  26523  dchrinvcl  26524  dchrptlem2  26536  dchrptlem3  26537  dchrsum2  26539  sumdchr2  26541  dchr2sum  26544  axtgcont1  27209  tgjustc1  27216  tgjustc2  27217  tglowdim1  27241  tgldimor  27243  tgldim0eq  27244  iscgrgd  27254  isismt  27275  tglnfn  27288  tglnunirn  27289  tglngval  27292  legval  27325  ishlg  27343  hlcgrex  27357  hlcgreulem  27358  mirval  27396  midexlem  27433  israg  27438  perpln1  27451  perpln2  27452  isperp  27453  ishpg  27500  midf  27517  ismidb  27519  lmif  27526  islmib  27528  iscgra  27550  isinag  27579  isleag  27588  iseqlg  27608  ttgval  27616  ttgvalOLD  27617  ttgitvval  27629  setsvtx  27785  uhgrunop  27825  incistruhgr  27829  upgrunop  27869  umgrunop  27871  usgriedgleord  27975  uspgredgleord  27979  uhgr0vsize0  27986  lfuhgr1v0e  28001  uhgrspanop  28043  upgrspanop  28044  umgrspanop  28045  usgrspanop  28046  uhgrspan1lem1  28047  upgrres1lem1  28056  usgredgffibi  28071  fusgredgfi  28072  usgr1v0e  28073  nbgr2vtx1edg  28097  nbuhgr2vtx1edgb  28099  nbfusgrlevtxm1  28124  nbfusgrlevtxm2  28125  uvtx01vtx  28144  cplgr1vlem  28176  cplgr1v  28177  cusgrsize2inds  28200  cusgrfilem3  28204  sizusglecusg  28210  fusgrmaxsize  28211  vtxdgfval  28214  vtxdun  28228  vtxd0nedgb  28235  p1evtxdeqlem  28259  p1evtxdeq  28260  p1evtxdp1  28261  usgrvd0nedg  28280  vtxdginducedm1lem1  28286  vtxdginducedm1lem4  28289  vtxdginducedm1  28290  vtxdginducedm1fi  28291  finsumvtxdg2ssteplem4  28295  rusgrnumwrdl2  28333  wksfval  28356  iswlkg  28360  wlkonprop  28405  wlkp1lem3  28422  wlkp1lem8  28427  wlkp1  28428  wksonproplem  28451  wksonproplemOLD  28452  wwlks  28579  wwlksnon  28595  wspthsnon  28596  clwwlk  28726  0wlkonlem2  28862  conngrv2edg  28938  eupthp1  28959  eupth2eucrct  28960  eupthvdres  28978  eupth2lem3  28979  eupth2lemb  28980  3cyclfrgrrn  29029  frgrwopreglem1  29055  frgrwopreg1  29061  imsmetlem  29431  dipfval  29443  sspval  29464  islno  29494  nmooval  29504  nmounbseqi  29518  nmobndseqi  29520  0ofval  29528  0oval  29529  ajfval  29550  isph  29563  phpar  29565  ajval  29602  ubthlem1  29611  ubthlem2  29612  minvecolem4b  29619  minvecolem4  29621  minvecolem5  29622  hlex  29639  ressplusf  31612  ressnm  31613  oppglt  31617  ressprs  31618  oduprs  31619  ismnt  31638  mgcval  31642  gsummptres  31689  gsummptres2  31690  gsumpart  31692  gsumhashmul  31693  inftmrel  31811  isinftm  31812  gsumvsca1  31856  ress1r  31863  rdivmuldivd  31865  ringinvval  31866  dvrcan5  31867  rmfsupp2  31869  fldgenval  31875  ofldlt1  31902  resvsca  31915  quslmod  31940  islinds5  31950  ellspds  31951  elrsp  31956  linds2eq  31962  elringlsm  31968  lsmsnpridl  31973  grplsm0l  31978  qusima  31981  nsgmgc  31984  nsgqusf1o  31988  elrspunidl  31993  prmidl0  32013  idlsrgbas  32036  idlsrgplusg  32037  idlsrgmulr  32039  idlsrgtset  32040  rprmval  32051  fply1  32054  evls1expd  32057  evls1fpws  32059  evls1muld  32061  dimval  32084  dimvalfi  32085  lvecdim0  32088  isalgnb  32146  mdetpmtr1  32178  rspectopn  32222  zarcls0  32223  zarcls  32229  zartopn  32230  zarmxt1  32235  rhmpreimacnlem  32239  rhmpreimacn  32240  pstmfval  32251  ordtrest2NEW  32278  ordtconnlem1  32279  fsumcvg4  32305  pl1cn  32310  qqhval  32329  sibf0  32708  sitgclg  32716  sitgaddlemb  32722  eulerpartlemgvv  32750  afsval  33058  pthhashvtx  33495  usgrcyclgt2v  33499  cusgr3cyclex  33504  acycgr2v  33518  cusgracyclt3v  33524  mrsubfval  33876  mrsubcv  33878  mrsubff  33880  mrsubrn  33881  elmrsubrn  33888  msubfval  33892  msubff  33898  mpstval  33903  elmpst  33904  msrval  33906  mstaval  33912  msubvrs  33928  mclsssvlem  33930  mclsval  33931  mclsind  33938  mppsval  33940  climlec3  34097  sdclem2  36097  sdclem1  36098  caures  36115  heiborlem3  36168  heibor  36176  grpokerinj  36248  rngoi  36254  dvrunz  36309  isdrngo1  36311  isdrngo2  36313  isrngohom  36320  idlval  36368  isidl  36369  0idl  36380  0rngo  36382  divrngidl  36383  smprngopr  36407  igenval  36416  lshpset  37336  lsatset  37348  lcvfbr  37378  islfl  37418  lfl0f  37427  lfl1  37428  lfladd0l  37432  lflnegl  37434  lflvscl  37435  lflvsdi1  37436  lflvsdi2  37437  lflvsdi2a  37438  lflvsass  37439  lfl0sc  37440  lflsc0N  37441  lfl1sc  37442  lkr0f  37452  lkrsc  37455  eqlkr2  37458  ldualvbase  37484  ldualfvadd  37486  ldualvaddval  37489  ldualsca  37490  ldualfvs  37494  ldualvsval  37496  isopos  37538  cmtfvalN  37568  cvrfval  37626  pats  37643  glbconNOLD  37736  llnset  37864  lplnset  37888  lvolset  37931  lineset  38097  isline  38098  pointsetN  38100  psubspset  38103  ispsubsp  38104  pmapval  38116  paddfval  38156  paddval  38157  pclfvalN  38248  pclvalN  38249  polfvalN  38263  polvalN  38264  psubclsetN  38295  ispsubclN  38296  watvalN  38352  lhpset  38354  lautset  38441  islaut  38442  pautsetN  38457  ispautN  38458  ldilset  38468  ltrnset  38477  dilsetN  38512  cdleme26e  38718  cdleme26eALTN  38720  cdleme26fALTN  38721  cdleme26f  38722  cdleme26f2ALTN  38723  cdleme26f2  38724  cdlemefs32sn1aw  38773  cdleme43fsv1snlem  38779  cdleme41sn3a  38792  cdleme32a  38800  cdleme40m  38826  cdleme40n  38827  cdleme42b  38837  tgrpbase  39105  tgrpopr  39106  istendo  39119  tendopl  39135  tendo02  39146  erngbase  39160  erngfplus  39161  erngfmul  39164  erngbase-rN  39168  erngfplus-rN  39169  erngfmul-rN  39172  cdlemk36  39272  cdlemkid  39295  dvasca  39365  dvavbase  39372  dvafvadd  39373  dvafvsca  39375  diafval  39390  diaval  39391  dvhsca  39441  dvhvbase  39446  dvhfvadd  39450  dvhfvsca  39459  docafvalN  39481  docavalN  39482  djafvalN  39493  djavalN  39494  dibfval  39500  dibopelvalN  39502  dibopelval2  39504  dibelval3  39506  diblsmopel  39530  dicfval  39534  dicval  39535  cdlemn11a  39566  dihvalcqpre  39594  dihopelvalcpre  39607  dihord6apre  39615  dihpN  39695  dochfval  39709  dochval  39710  djhfval  39756  djhval  39757  islpolN  39842  lpolconN  39846  dochpolN  39849  lcfrlem9  39909  lcd0vvalN  39972  mapdval  39987  mapd1o  40007  mapdunirnN  40009  mapdhval  40083  mapdhval0  40084  hvmapfval  40118  hvmapval  40119  hdmap1fval  40155  hdmap1vallem  40156  hgmapfval  40245  hlhilset  40293  hlhilbase  40295  hlhilplus  40296  hlhilvsca  40310  hlhilip  40311  hlhilnvl  40313  hlhillsm  40319  hlhillcs  40321  frlmfielbas  40576  sn-0subg  40593  frlm0vald  40619  evlsval3  40627  evlsbagval  40630  fsuppind  40634  fsuppssind  40637  mhpind  40638  mhphf  40640  islssfgi  41265  pwssplit4  41282  frlmpwfi  41291  mendplusgfval  41378  mendmulrfval  41380  mendvscafval  41383  idomrootle  41388  idomodle  41389  deg1mhm  41400  mnringelbased  42259  mnring0g2d  42265  mnringmulrd  42266  mnringmulrcld  42273  dvgrat  42357  uzmptshftfval  42391  climexp  43600  climinf  43601  climneg  43605  climdivf  43607  climconstmpt  43653  climresmpt  43654  climsubmpt  43655  fnlimfvre  43669  limsupvaluz  43703  limsupequzmpt2  43713  climuzlem  43738  climisp  43741  climxrrelem  43744  climxrre  43745  limsupgtlem  43772  liminflelimsupuz  43780  liminfgelimsupuz  43783  liminfequzmpt2  43786  liminfvaluz  43787  limsupvaluz3  43793  climliminflimsupd  43796  liminfreuzlem  43797  liminfltlem  43799  liminflimsupclim  43802  liminflbuz2  43810  liminfpnfuz  43811  xlimclim2lem  43834  climxlim2  43841  sge0isum  44422  sge0uzfsumgt  44439  sge0seq  44441  meaiunlelem  44463  caragendifcl  44509  omeiunle  44512  omeiunltfirp  44514  carageniuncl  44518  caragensal  44520  opnssborel  44630  smflimlem6  44771  smfpimcc  44803  smflimmpt  44805  smflimsuplem4  44818  smflimsuplem6  44820  smflimsuplem8  44822  smfliminflem  44825  isomuspgrlem2  45775  ushrisomgr  45783  upwlksfval  45787  isupwlkg  45789  ismgmhm  45827  issubmgm2  45834  submgmacs  45848  copisnmnd  45853  0ringdif  45918  rnghmval  45939  isrnghm  45940  c0snmgmhm  45962  c0snmhm  45963  zrrnghm  45965  zlidlring  45976  cznrng  46003  cznnring  46004  rngchomfvalALTV  46032  rngccofvalALTV  46035  rngccatidALTV  46037  ringchomfvalALTV  46095  ringccofvalALTV  46098  ringccatidALTV  46100  rngcrescrhm  46133  rngcrescrhmALTV  46151  ofaddmndmap  46169  suppmptcfin  46205  mptcfsupp  46206  dmatALTbas  46232  lcoop  46242  linccl  46245  lcosn0  46251  lincvalsc0  46252  lcoc0  46253  linc0scn0  46254  linc1  46256  lincscmcl  46263  islinindfis  46280  lincext1  46285  lincext2  46286  lindslinindimp2lem2  46290  lindslinindimp2lem3  46291  lindsrng01  46299  snlindsntorlem  46301  snlindsntor  46302  ldepspr  46304  lincresunit1  46308  lincresunit2  46309  lines  46567  line  46568  rrxlines  46569  sphere  46583  rrxsphere  46584  functhinclem1  46811  thincciso  46819
  Copyright terms: Public domain W3C validator