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  subgacs  18895  nsgacs  18896  nmznsg  18902  eqgfval  18910  isghm  18940  gicen  18999  isga  19003  subgga  19012  orbstafun  19023  orbstaval  19024  orbsta  19025  cntzfval  19032  cntzval  19033  oppgplusfval  19058  symg2bas  19106  symgvalstruct  19110  symgvalstructOLD  19111  cayleylem2  19127  psgnfval  19214  odfval  19246  odinf  19276  dfod2  19277  pgpfi1  19306  pgp0  19307  sylow1lem2  19310  sylow3lem6  19343  lsmfval  19349  lsmvalx  19350  oppglsm  19353  pj1fval  19405  efglem  19427  efgrelexlemb  19461  efgcpbllemb  19466  frgpeccl  19472  frgpmhm  19476  vrgpval  19478  frgpuplem  19483  frgpupf  19484  frgpupval  19485  frgpup1  19486  frgpup3lem  19488  frgpnabllem2  19581  iscygodd  19594  prmcyg  19600  lt6abl  19601  gsumval3a  19609  gsumval3  19613  gsumzres  19615  gsumzcl2  19616  gsumzf1o  19618  gsumreidx  19623  gsumzaddlem  19627  gsumzadd  19628  gsumzsplit  19633  gsummptshft  19642  gsumzmhm  19643  gsumzoppg  19650  gsumzinv  19651  gsummptfidminv  19653  gsumsub  19654  gsumpt  19668  gsummptf1o  19669  gsum2dlem1  19676  gsum2dlem2  19677  gsum2d  19678  gsum2d2lem  19679  gsumxp2  19686  fsfnn0gsumfsffz  19689  nn0gsumfz  19690  gsummptnn0fz  19692  dprdfid  19725  dprdfinv  19727  dprdfadd  19728  dprdfeq0  19730  dmdprdsplitlem  19745  dpjidcl  19766  ablfacrplem  19773  ablfacrp  19774  ablfacrp2  19775  ablfac1a  19777  ablfac1b  19778  ablfac1c  19779  ablfac1eu  19781  pgpfaclem2  19790  ablfaclem2  19794  ablfaclem3  19795  2nsgsimpgd  19810  prmgrpsimpgd  19822  ablsimpgprmd  19823  mgpplusg  19829  mgpress  19840  mgpressOLD  19841  issrg  19848  ring1ne0  19938  gsumdixp  19956  pwsmgp  19965  opprmulfval  19974  dvdsrval  19997  isunit  20009  unitgrp  20019  unitlinv  20029  unitrinv  20030  dvrfval  20036  isdrng2  20121  drngmcl  20124  drngid2  20127  issubrg  20145  subrgugrp  20164  subrgacs  20190  sdrgacs  20191  cntzsdrg  20192  subdrgint  20193  isabv  20201  staffval  20229  islmod  20249  scaffval  20263  lcomfsupp  20285  mptscmfsupp0  20310  rmodislmod  20313  rmodislmodOLD  20314  lssset  20317  islss  20318  lsssn0  20331  lssacs  20351  lspfval  20357  lspval  20359  lspcl  20360  lspuni0  20394  lss0v  20400  0lmhm  20424  lmhmvsca  20429  islbs  20460  islbs3  20539  lbsextlem1  20542  lbsextlem3  20544  lbsextlem4  20545  lbsext  20547  rsp1  20617  2idlval  20626  qusrhm  20630  isnzr2  20656  isnzr2hash  20657  0ring  20663  01eq0ring  20665  0ring01eqbi  20666  rrgval  20680  rrgsupp  20684  expghm  20819  zrhrhmb  20834  zlmvsca  20849  zntoslem  20886  znfi  20889  znunithash  20894  psgnghm  20907  psgnghm2  20908  psgnevpmb  20914  ipffval  20975  ocvfval  20993  ocvval  20994  elocv  20995  thlbas  21023  thlbasOLD  21024  thlle  21025  thlleOLD  21026  thlleval  21027  thloc  21028  pjfval  21035  pjdm  21036  pjpm  21037  isobs  21049  frlmbas  21084  frlmbasf  21089  frlmvscafval  21095  frlmvscavalb  21099  frlmsslss2  21104  frlmip  21107  uvcvval  21115  uvcvvcl  21116  frlmssuvc2  21124  frlmsslsp  21125  ellspd  21131  elfilspd  21132  islinds2  21142  islindf4  21167  aspval  21199  psrbas  21269  psrelbas  21270  psrplusg  21272  psrmulr  21275  psrvscafval  21281  psrvscacl  21284  psr0lid  21286  psrlidm  21294  psrridm  21295  resspsradd  21307  resspsrmul  21308  resspsrvsca  21309  mvrval2  21313  mplsubglem  21327  mpllsslem  21328  mplsubrglem  21332  mpladd  21335  mplmul  21337  ressmpladd  21352  ressmplmul  21353  ressmplvsca  21354  mplmon  21358  mplmonmul  21359  mplcoe1  21360  opsrle  21370  opsrtoslem2  21385  mplmon2  21391  evlslem4  21406  psrbagev1  21407  psrbagev1OLD  21408  evlslem2  21411  evlslem3  21412  evlsval2  21419  selvval  21450  mhpval  21452  ismhp3  21455  coe1sfi  21506  coe1fsupp  21507  mptcoe1fsupp  21508  coe1ae0  21509  ressply1add  21523  ressply1mul  21524  ressply1vsca  21525  gsumply1subr  21527  psropprmul  21531  coe1tmmul2fv  21571  coe1pwmulfv  21573  ply1coe  21589  cply1coe0  21592  cply1coe0bi  21593  gsummoncoe1  21597  evls1fval  21607  evls1val  21608  evls1rhmlem  21609  evls1sca  21611  evls1gsumadd  21612  evls1gsummul  21613  evl1val  21617  evl1fval1lem  21618  fveval1fvcl  21621  evl1sca  21622  evl1var  21624  evl1addd  21629  evl1subd  21630  evl1muld  21631  evl1expd  21633  pf1f  21638  pf1mpf  21640  pf1ind  21643  evl1gsummul  21648  mamures  21661  mndvcl  21662  mamucl  21670  mamuvs1  21674  mamuvs2  21675  matbas2d  21694  matecl  21696  mamumat1cl  21710  mat1comp  21711  mamulid  21712  mamurid  21713  mat1ov  21719  matsc  21721  mat1dimelbas  21742  mat1dimmul  21747  mat1f1o  21749  dmatval  21763  dmatmulcl  21771  scmatval  21775  scmatscmiddistr  21779  mavmulcl  21818  1mavmul  21819  marrepfval  21831  marrepeval  21834  marepvfval  21836  submafval  21850  mdetfval  21857  mdetunilem9  21891  mdetuni0  21892  m2detleiblem3  21900  m2detleiblem4  21901  minmar1fval  21917  minmar1eval  21920  symgmatr01  21925  gsummatr01lem3  21928  gsummatr01  21930  smadiadetlem1a  21934  smadiadetlem3  21939  invrvald  21947  cpmat  21980  mat2pmatfval  21994  mat2pmatbas  21997  decpmatfsupp  22040  decpmatmulsumfsupp  22044  pmatcollpw3lem  22054  pmatcollpw3fi1lem2  22058  pm2mpval  22066  mply1topmatcl  22076  chmatval  22100  chpmatfval  22101  chfacffsupp  22127  chfacfscmul0  22129  chfacfscmulfsupp  22130  chfacfpmmul0  22133  chfacfpmmulfsupp  22134  cpmidpmatlem2  22142  cpmadumatpolylem1  22152  imastopn  22993  uzrest  23170  tmdgsum2  23369  distgp  23372  indistgp  23373  snclseqg  23389  tsmsval  23404  tsms0  23415  tsmsres  23417  tsmsxplem1  23426  tsmsxplem2  23427  ussid  23534  isusp  23535  ressust  23537  cnextucn  23577  prdsxmetlem  23643  nrmmetd  23852  nmfval  23866  tngds  23933  tngdsOLD  23934  tngnm  23937  tngngp2  23938  tngngpd  23939  tngngp  23940  tngngp3  23942  nmo0  24021  xrrest  24092  climcncf  24185  cphsubrglem  24463  cphcjcl  24469  tcphex  24503  ipcau2  24520  cmsss  24637  rrxip  24676  minveclem4a  24716  minveclem4  24718  mbflimsup  24952  mbflim  24954  mdegfval  25349  mdegleb  25351  mdegldg  25353  deg1val  25383  uc1pval  25426  mon1pval  25428  q1pval  25440  r1pval  25443  ply1remlem  25449  ply1rem  25450  fta1glem1  25452  fta1glem2  25453  fta1blem  25455  ig1pval  25459  elqaalem3  25603  ulmcau  25676  ulmdvlem1  25681  ulmdvlem3  25683  mbfulm  25687  itgulm  25689  dchrplusg  26517  dchrmulid2  26522  dchrinvcl  26523  dchrptlem2  26535  dchrptlem3  26536  dchrsum2  26538  sumdchr2  26540  dchr2sum  26543  axtgcont1  27196  tgjustc1  27203  tgjustc2  27204  tglowdim1  27228  tgldimor  27230  tgldim0eq  27231  iscgrgd  27241  isismt  27262  tglnfn  27275  tglnunirn  27276  tglngval  27279  legval  27312  ishlg  27330  hlcgrex  27344  hlcgreulem  27345  mirval  27383  midexlem  27420  israg  27425  perpln1  27438  perpln2  27439  isperp  27440  ishpg  27487  midf  27504  ismidb  27506  lmif  27513  islmib  27515  iscgra  27537  isinag  27566  isleag  27575  iseqlg  27595  ttgval  27603  ttgvalOLD  27604  ttgitvval  27616  setsvtx  27772  uhgrunop  27812  incistruhgr  27816  upgrunop  27856  umgrunop  27858  usgriedgleord  27962  uspgredgleord  27966  uhgr0vsize0  27973  lfuhgr1v0e  27988  uhgrspanop  28030  upgrspanop  28031  umgrspanop  28032  usgrspanop  28033  uhgrspan1lem1  28034  upgrres1lem1  28043  usgredgffibi  28058  fusgredgfi  28059  usgr1v0e  28060  nbgr2vtx1edg  28084  nbuhgr2vtx1edgb  28086  nbfusgrlevtxm1  28111  nbfusgrlevtxm2  28112  uvtx01vtx  28131  cplgr1vlem  28163  cplgr1v  28164  cusgrsize2inds  28187  cusgrfilem3  28191  sizusglecusg  28197  fusgrmaxsize  28198  vtxdgfval  28201  vtxdun  28215  vtxd0nedgb  28222  p1evtxdeqlem  28246  p1evtxdeq  28247  p1evtxdp1  28248  usgrvd0nedg  28267  vtxdginducedm1lem1  28273  vtxdginducedm1lem4  28276  vtxdginducedm1  28277  vtxdginducedm1fi  28278  finsumvtxdg2ssteplem4  28282  rusgrnumwrdl2  28320  wksfval  28343  iswlkg  28347  wlkonprop  28392  wlkp1lem3  28409  wlkp1lem8  28414  wlkp1  28415  wksonproplem  28438  wksonproplemOLD  28439  wwlks  28566  wwlksnon  28582  wspthsnon  28583  clwwlk  28713  0wlkonlem2  28849  conngrv2edg  28925  eupthp1  28946  eupth2eucrct  28947  eupthvdres  28965  eupth2lem3  28966  eupth2lemb  28967  3cyclfrgrrn  29016  frgrwopreglem1  29042  frgrwopreg1  29048  imsmetlem  29418  dipfval  29430  sspval  29451  islno  29481  nmooval  29491  nmounbseqi  29505  nmobndseqi  29507  0ofval  29515  0oval  29516  ajfval  29537  isph  29550  phpar  29552  ajval  29589  ubthlem1  29598  ubthlem2  29599  minvecolem4b  29606  minvecolem4  29608  minvecolem5  29609  hlex  29626  ressplusf  31599  ressnm  31600  oppglt  31604  ressprs  31605  oduprs  31606  ismnt  31625  mgcval  31629  gsummptres  31676  gsummptres2  31677  gsumpart  31679  gsumhashmul  31680  inftmrel  31798  isinftm  31799  gsumvsca1  31843  ress1r  31850  rdivmuldivd  31852  ringinvval  31853  dvrcan5  31854  rmfsupp2  31856  fldgenval  31862  ofldlt1  31889  resvsca  31902  quslmod  31927  islinds5  31937  ellspds  31938  elrsp  31943  linds2eq  31949  elringlsm  31955  lsmsnpridl  31960  grplsm0l  31965  qusima  31968  nsgmgc  31971  nsgqusf1o  31975  elrspunidl  31980  prmidl0  32000  idlsrgbas  32023  idlsrgplusg  32024  idlsrgmulr  32026  idlsrgtset  32027  rprmval  32038  fply1  32041  evls1expd  32044  evls1fpws  32046  evls1muld  32048  dimval  32071  dimvalfi  32072  lvecdim0  32075  isalgnb  32133  mdetpmtr1  32165  rspectopn  32209  zarcls0  32210  zarcls  32216  zartopn  32217  zarmxt1  32222  rhmpreimacnlem  32226  rhmpreimacn  32227  pstmfval  32238  ordtrest2NEW  32265  ordtconnlem1  32266  fsumcvg4  32292  pl1cn  32297  qqhval  32316  sibf0  32695  sitgclg  32703  sitgaddlemb  32709  eulerpartlemgvv  32737  afsval  33045  pthhashvtx  33482  usgrcyclgt2v  33486  cusgr3cyclex  33491  acycgr2v  33505  cusgracyclt3v  33511  mrsubfval  33863  mrsubcv  33865  mrsubff  33867  mrsubrn  33868  elmrsubrn  33875  msubfval  33879  msubff  33885  mpstval  33890  elmpst  33891  msrval  33893  mstaval  33899  msubvrs  33915  mclsssvlem  33917  mclsval  33918  mclsind  33925  mppsval  33927  climlec3  34084  sdclem2  36087  sdclem1  36088  caures  36105  heiborlem3  36158  heibor  36166  grpokerinj  36238  rngoi  36244  dvrunz  36299  isdrngo1  36301  isdrngo2  36303  isrngohom  36310  idlval  36358  isidl  36359  0idl  36370  0rngo  36372  divrngidl  36373  smprngopr  36397  igenval  36406  lshpset  37326  lsatset  37338  lcvfbr  37368  islfl  37408  lfl0f  37417  lfl1  37418  lfladd0l  37422  lflnegl  37424  lflvscl  37425  lflvsdi1  37426  lflvsdi2  37427  lflvsdi2a  37428  lflvsass  37429  lfl0sc  37430  lflsc0N  37431  lfl1sc  37432  lkr0f  37442  lkrsc  37445  eqlkr2  37448  ldualvbase  37474  ldualfvadd  37476  ldualvaddval  37479  ldualsca  37480  ldualfvs  37484  ldualvsval  37486  isopos  37528  cmtfvalN  37558  cvrfval  37616  pats  37633  glbconNOLD  37726  llnset  37854  lplnset  37878  lvolset  37921  lineset  38087  isline  38088  pointsetN  38090  psubspset  38093  ispsubsp  38094  pmapval  38106  paddfval  38146  paddval  38147  pclfvalN  38238  pclvalN  38239  polfvalN  38253  polvalN  38254  psubclsetN  38285  ispsubclN  38286  watvalN  38342  lhpset  38344  lautset  38431  islaut  38432  pautsetN  38447  ispautN  38448  ldilset  38458  ltrnset  38467  dilsetN  38502  cdleme26e  38708  cdleme26eALTN  38710  cdleme26fALTN  38711  cdleme26f  38712  cdleme26f2ALTN  38713  cdleme26f2  38714  cdlemefs32sn1aw  38763  cdleme43fsv1snlem  38769  cdleme41sn3a  38782  cdleme32a  38790  cdleme40m  38816  cdleme40n  38817  cdleme42b  38827  tgrpbase  39095  tgrpopr  39096  istendo  39109  tendopl  39125  tendo02  39136  erngbase  39150  erngfplus  39151  erngfmul  39154  erngbase-rN  39158  erngfplus-rN  39159  erngfmul-rN  39162  cdlemk36  39262  cdlemkid  39285  dvasca  39355  dvavbase  39362  dvafvadd  39363  dvafvsca  39365  diafval  39380  diaval  39381  dvhsca  39431  dvhvbase  39436  dvhfvadd  39440  dvhfvsca  39449  docafvalN  39471  docavalN  39472  djafvalN  39483  djavalN  39484  dibfval  39490  dibopelvalN  39492  dibopelval2  39494  dibelval3  39496  diblsmopel  39520  dicfval  39524  dicval  39525  cdlemn11a  39556  dihvalcqpre  39584  dihopelvalcpre  39597  dihord6apre  39605  dihpN  39685  dochfval  39699  dochval  39700  djhfval  39746  djhval  39747  islpolN  39832  lpolconN  39836  dochpolN  39839  lcfrlem9  39899  lcd0vvalN  39962  mapdval  39977  mapd1o  39997  mapdunirnN  39999  mapdhval  40073  mapdhval0  40074  hvmapfval  40108  hvmapval  40109  hdmap1fval  40145  hdmap1vallem  40146  hgmapfval  40235  hlhilset  40283  hlhilbase  40285  hlhilplus  40286  hlhilvsca  40300  hlhilip  40301  hlhilnvl  40303  hlhillsm  40309  hlhillcs  40311  frlmfielbas  40566  frlm0vald  40597  evlsval3  40605  evlsbagval  40608  fsuppind  40612  fsuppssind  40615  mhpind  40616  mhphf  40618  islssfgi  41233  pwssplit4  41250  frlmpwfi  41259  mendplusgfval  41346  mendmulrfval  41348  mendvscafval  41351  idomrootle  41356  idomodle  41357  deg1mhm  41368  mnringelbased  42227  mnring0g2d  42233  mnringmulrd  42234  mnringmulrcld  42241  dvgrat  42325  uzmptshftfval  42359  climexp  43568  climinf  43569  climneg  43573  climdivf  43575  climconstmpt  43621  climresmpt  43622  climsubmpt  43623  fnlimfvre  43637  limsupvaluz  43671  limsupequzmpt2  43681  climuzlem  43706  climisp  43709  climxrrelem  43712  climxrre  43713  limsupgtlem  43740  liminflelimsupuz  43748  liminfgelimsupuz  43751  liminfequzmpt2  43754  liminfvaluz  43755  limsupvaluz3  43761  climliminflimsupd  43764  liminfreuzlem  43765  liminfltlem  43767  liminflimsupclim  43770  liminflbuz2  43778  liminfpnfuz  43779  xlimclim2lem  43802  climxlim2  43809  sge0isum  44390  sge0uzfsumgt  44407  sge0seq  44409  meaiunlelem  44431  caragendifcl  44477  omeiunle  44480  omeiunltfirp  44482  carageniuncl  44486  caragensal  44488  opnssborel  44598  smflimlem6  44739  smfpimcc  44771  smflimmpt  44773  smflimsuplem4  44786  smflimsuplem6  44788  smflimsuplem8  44790  smfliminflem  44793  isomuspgrlem2  45743  ushrisomgr  45751  upwlksfval  45755  isupwlkg  45757  ismgmhm  45795  issubmgm2  45802  submgmacs  45816  copisnmnd  45821  0ringdif  45886  rnghmval  45907  isrnghm  45908  c0snmgmhm  45930  c0snmhm  45931  zrrnghm  45933  zlidlring  45944  cznrng  45971  cznnring  45972  rngchomfvalALTV  46000  rngccofvalALTV  46003  rngccatidALTV  46005  ringchomfvalALTV  46063  ringccofvalALTV  46066  ringccatidALTV  46068  rngcrescrhm  46101  rngcrescrhmALTV  46119  ofaddmndmap  46137  suppmptcfin  46173  mptcfsupp  46174  dmatALTbas  46200  lcoop  46210  linccl  46213  lcosn0  46219  lincvalsc0  46220  lcoc0  46221  linc0scn0  46222  linc1  46224  lincscmcl  46231  islinindfis  46248  lincext1  46253  lincext2  46254  lindslinindimp2lem2  46258  lindslinindimp2lem3  46259  lindsrng01  46267  snlindsntorlem  46269  snlindsntor  46270  ldepspr  46272  lincresunit1  46276  lincresunit2  46277  lines  46535  line  46536  rrxlines  46537  sphere  46551  rrxsphere  46552  functhinclem1  46779  thincciso  46787
  Copyright terms: Public domain W3C validator