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

Theorem fvexi 6797
Description: The value of a class exists. Inference form of fvex 6796. (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 6796 . 2 (𝐹𝐵) ∈ V
31, 2eqeltri 2836 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2107  Vcvv 3433  cfv 6437
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-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-sn 4563  df-pr 4565  df-uni 4841  df-iota 6395  df-fv 6445
This theorem is referenced by:  mptfvmpt  7113  ovex  7317  mapfienlem1  9173  climle  15358  climsup  15390  iserabs  15536  isumshft  15560  explecnv  15586  prodfclim1  15614  ressbas  16956  ressbasOLD  16957  ressbas2  16958  ressid  16963  ressval3d  16965  ressval3dOLD  16966  topnid  17155  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  prdsip  17181  prdsle  17182  prdsds  17184  prdshom  17187  prdsco  17188  pwselbasb  17208  pwsvscafval  17214  pwssca  17216  pwssnf1o  17218  imassca  17239  imasvsca  17240  imasle  17243  xpsrnbas  17291  xpssca  17296  xpsvsca  17297  isacs2  17371  homffval  17408  comfffval  17416  oppchomfval  17432  oppchomfvalOLD  17433  oppccofval  17435  oppccatid  17439  monfval  17453  oppcmon  17459  sectffval  17471  invffval  17479  rescbas  17550  rescbasOLD  17551  reschom  17552  rescco  17554  resccoOLD  17555  fullsubc  17574  isfunc  17588  isfuncd  17589  idfu2nd  17601  idfu1st  17603  cofu1st  17607  cofu2nd  17609  fucco  17689  fucid  17698  invfuc  17701  initoval  17717  termoval  17718  homafval  17753  arwval  17767  coafval  17788  coapm  17795  setccatid  17808  catchomfval  17826  catccofval  17828  catccatid  17830  elestrchom  17853  estrccatid  17857  xpcbas  17904  xpchomfval  17905  xpccofval  17908  1stf1  17918  1stf2  17919  2ndf1  17921  2ndf2  17922  prf1  17926  prf2fval  17927  evlf2  17945  evlf1  17947  curf1fval  17951  curf11  17953  curf12  17954  curf1cl  17955  curf2  17956  curf2cl  17958  hof2fval  17982  yonedalem4a  18002  yonedalem4c  18004  yonedalem3  18007  yonedainv  18008  isdrs  18028  ispos  18041  odupos  18055  pltfval  18058  lubfval  18077  lubeldm  18080  lubval  18083  glbfval  18090  glbeldm  18093  glbval  18096  odulub  18134  odujoin  18135  oduglb  18136  odumeet  18137  clatlem  18229  clatlubcl2  18231  clatglbcl2  18233  isdlat  18249  ipolt  18262  ipopos  18263  isacs4lem  18271  plusffval  18341  issstrmgm  18346  gsumvalx  18369  gsumval  18370  issubmnd  18421  ress0g  18422  ismhm  18441  0subm  18465  0mhm  18467  submacs  18474  pwsdiagmhm  18478  gsumz  18483  frmdplusg  18502  efmndplusg  18528  efmndmgm  18533  smndex1mgm  18555  grpinvfval  18627  grpsubfval  18632  grpsubfvalALT  18633  mulgfval  18711  mulgfvalALT  18712  mulgval  18713  issubg  18764  0subg  18789  subgacs  18798  nsgacs  18799  nmznsg  18805  eqgfval  18813  isghm  18843  gicen  18902  isga  18906  subgga  18915  orbstafun  18926  orbstaval  18927  orbsta  18928  cntzfval  18935  cntzval  18936  oppgplusfval  18961  symg2bas  19009  symgvalstruct  19013  symgvalstructOLD  19014  cayleylem2  19030  psgnfval  19117  odfval  19149  odinf  19179  dfod2  19180  pgpfi1  19209  pgp0  19210  sylow1lem2  19213  sylow3lem6  19246  lsmfval  19252  lsmvalx  19253  oppglsm  19256  pj1fval  19309  efglem  19331  efgrelexlemb  19365  efgcpbllemb  19370  frgpeccl  19376  frgpmhm  19380  vrgpval  19382  frgpuplem  19387  frgpupf  19388  frgpupval  19389  frgpup1  19390  frgpup3lem  19392  frgpnabllem2  19484  iscygodd  19497  prmcyg  19504  lt6abl  19505  gsumval3a  19513  gsumval3  19517  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumreidx  19527  gsumzaddlem  19531  gsumzadd  19532  gsumzsplit  19537  gsummptshft  19546  gsumzmhm  19547  gsumzoppg  19554  gsumzinv  19555  gsummptfidminv  19557  gsumsub  19558  gsumpt  19572  gsummptf1o  19573  gsum2dlem1  19580  gsum2dlem2  19581  gsum2d  19582  gsum2d2lem  19583  gsumxp2  19590  fsfnn0gsumfsffz  19593  nn0gsumfz  19594  gsummptnn0fz  19596  dprdfid  19629  dprdfinv  19631  dprdfadd  19632  dprdfeq0  19634  dmdprdsplitlem  19649  dpjidcl  19670  ablfacrplem  19677  ablfacrp  19678  ablfacrp2  19679  ablfac1a  19681  ablfac1b  19682  ablfac1c  19683  ablfac1eu  19685  pgpfaclem2  19694  ablfaclem2  19698  ablfaclem3  19699  2nsgsimpgd  19714  prmgrpsimpgd  19726  ablsimpgprmd  19727  mgpplusg  19733  mgpress  19744  mgpressOLD  19745  issrg  19752  ring1ne0  19839  gsumdixp  19857  pwsmgp  19866  opprmulfval  19873  dvdsrval  19896  isunit  19908  unitgrp  19918  unitlinv  19928  unitrinv  19929  dvrfval  19935  isdrng2  20010  drngmcl  20013  drngid2  20016  issubrg  20033  subrgugrp  20052  subrgacs  20077  sdrgacs  20078  cntzsdrg  20079  subdrgint  20080  isabv  20088  staffval  20116  islmod  20136  scaffval  20150  lcomfsupp  20172  mptscmfsupp0  20197  rmodislmod  20200  rmodislmodOLD  20201  lssset  20204  islss  20205  lsssn0  20218  lssacs  20238  lspfval  20244  lspval  20246  lspcl  20247  lspuni0  20281  lss0v  20287  0lmhm  20311  lmhmvsca  20316  islbs  20347  islbs3  20426  lbsextlem1  20429  lbsextlem3  20431  lbsextlem4  20432  lbsext  20434  rsp1  20504  2idlval  20513  qusrhm  20517  isnzr2  20543  isnzr2hash  20544  0ring  20550  01eq0ring  20552  0ring01eqbi  20553  rrgval  20567  rrgsupp  20571  expghm  20706  zrhrhmb  20721  zlmvsca  20736  zntoslem  20773  znfi  20776  znunithash  20781  psgnghm  20794  psgnghm2  20795  psgnevpmb  20801  ipffval  20862  ocvfval  20880  ocvval  20881  elocv  20882  thlbas  20910  thlbasOLD  20911  thlle  20912  thlleOLD  20913  thlleval  20914  thloc  20915  pjfval  20922  pjdm  20923  pjpm  20924  isobs  20936  frlmbas  20971  frlmbasf  20976  frlmvscafval  20982  frlmvscavalb  20986  frlmsslss2  20991  frlmip  20994  uvcvval  21002  uvcvvcl  21003  frlmssuvc2  21011  frlmsslsp  21012  ellspd  21018  elfilspd  21019  islinds2  21029  islindf4  21054  aspval  21086  psrbas  21156  psrelbas  21157  psrplusg  21159  psrmulr  21162  psrvscafval  21168  psrvscacl  21171  psr0lid  21173  psrlidm  21181  psrridm  21182  resspsradd  21194  resspsrmul  21195  resspsrvsca  21196  mvrval2  21200  mplsubglem  21214  mpllsslem  21215  mplsubrglem  21219  mpladd  21222  mplmul  21224  ressmpladd  21239  ressmplmul  21240  ressmplvsca  21241  mplmon  21245  mplmonmul  21246  mplcoe1  21247  opsrle  21257  opsrtoslem2  21272  mplmon2  21278  evlslem4  21293  psrbagev1  21294  psrbagev1OLD  21295  evlslem2  21298  evlslem3  21299  evlsval2  21306  selvval  21337  mhpval  21339  ismhp3  21342  coe1sfi  21393  coe1fsupp  21394  mptcoe1fsupp  21395  coe1ae0  21396  ressply1add  21410  ressply1mul  21411  ressply1vsca  21412  gsumply1subr  21414  psropprmul  21418  coe1tmmul2fv  21458  coe1pwmulfv  21460  ply1coe  21476  cply1coe0  21479  cply1coe0bi  21480  gsummoncoe1  21484  evls1fval  21494  evls1val  21495  evls1rhmlem  21496  evls1sca  21498  evls1gsumadd  21499  evls1gsummul  21500  evl1val  21504  evl1fval1lem  21505  fveval1fvcl  21508  evl1sca  21509  evl1var  21511  evl1addd  21516  evl1subd  21517  evl1muld  21518  evl1expd  21520  pf1f  21525  pf1mpf  21527  pf1ind  21530  evl1gsummul  21535  mamures  21548  mndvcl  21549  mamucl  21557  mamuvs1  21561  mamuvs2  21562  matbas2d  21581  matecl  21583  mamumat1cl  21597  mat1comp  21598  mamulid  21599  mamurid  21600  mat1ov  21606  matsc  21608  mat1dimelbas  21629  mat1dimmul  21634  mat1f1o  21636  dmatval  21650  dmatmulcl  21658  scmatval  21662  scmatscmiddistr  21666  mavmulcl  21705  1mavmul  21706  marrepfval  21718  marrepeval  21721  marepvfval  21723  submafval  21737  mdetfval  21744  mdetunilem9  21778  mdetuni0  21779  m2detleiblem3  21787  m2detleiblem4  21788  minmar1fval  21804  minmar1eval  21807  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01  21817  smadiadetlem1a  21821  smadiadetlem3  21826  invrvald  21834  cpmat  21867  mat2pmatfval  21881  mat2pmatbas  21884  decpmatfsupp  21927  decpmatmulsumfsupp  21931  pmatcollpw3lem  21941  pmatcollpw3fi1lem2  21945  pm2mpval  21953  mply1topmatcl  21963  chmatval  21987  chpmatfval  21988  chfacffsupp  22014  chfacfscmul0  22016  chfacfscmulfsupp  22017  chfacfpmmul0  22020  chfacfpmmulfsupp  22021  cpmidpmatlem2  22029  cpmadumatpolylem1  22039  imastopn  22880  uzrest  23057  tmdgsum2  23256  distgp  23259  indistgp  23260  snclseqg  23276  tsmsval  23291  tsms0  23302  tsmsres  23304  tsmsxplem1  23313  tsmsxplem2  23314  ussid  23421  isusp  23422  ressust  23424  cnextucn  23464  prdsxmetlem  23530  nrmmetd  23739  nmfval  23753  tngds  23820  tngdsOLD  23821  tngnm  23824  tngngp2  23825  tngngpd  23826  tngngp  23827  tngngp3  23829  nmo0  23908  xrrest  23979  climcncf  24072  cphsubrglem  24350  cphcjcl  24356  tcphex  24390  ipcau2  24407  cmsss  24524  rrxip  24563  minveclem4a  24603  minveclem4  24605  mbflimsup  24839  mbflim  24841  mdegfval  25236  mdegleb  25238  mdegldg  25240  deg1val  25270  uc1pval  25313  mon1pval  25315  q1pval  25327  r1pval  25330  ply1remlem  25336  ply1rem  25337  fta1glem1  25339  fta1glem2  25340  fta1blem  25342  ig1pval  25346  elqaalem3  25490  ulmcau  25563  ulmdvlem1  25568  ulmdvlem3  25570  mbfulm  25574  itgulm  25576  dchrplusg  26404  dchrmulid2  26409  dchrinvcl  26410  dchrptlem2  26422  dchrptlem3  26423  dchrsum2  26425  sumdchr2  26427  dchr2sum  26430  axtgcont1  26838  tgjustc1  26845  tgjustc2  26846  tglowdim1  26870  tgldimor  26872  tgldim0eq  26873  iscgrgd  26883  isismt  26904  tglnfn  26917  tglnunirn  26918  tglngval  26921  legval  26954  ishlg  26972  hlcgrex  26986  hlcgreulem  26987  mirval  27025  midexlem  27062  israg  27067  perpln1  27080  perpln2  27081  isperp  27082  ishpg  27129  midf  27146  ismidb  27148  lmif  27155  islmib  27157  iscgra  27179  isinag  27208  isleag  27217  iseqlg  27237  ttgval  27245  ttgvalOLD  27246  ttgitvval  27258  setsvtx  27414  uhgrunop  27454  incistruhgr  27458  upgrunop  27498  umgrunop  27500  usgriedgleord  27604  uspgredgleord  27608  uhgr0vsize0  27615  lfuhgr1v0e  27630  uhgrspanop  27672  upgrspanop  27673  umgrspanop  27674  usgrspanop  27675  uhgrspan1lem1  27676  upgrres1lem1  27685  usgredgffibi  27700  fusgredgfi  27701  usgr1v0e  27702  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  nbfusgrlevtxm1  27753  nbfusgrlevtxm2  27754  uvtx01vtx  27773  cplgr1vlem  27805  cplgr1v  27806  cusgrsize2inds  27829  cusgrfilem3  27833  sizusglecusg  27839  fusgrmaxsize  27840  vtxdgfval  27843  vtxdun  27857  vtxd0nedgb  27864  p1evtxdeqlem  27888  p1evtxdeq  27889  p1evtxdp1  27890  usgrvd0nedg  27909  vtxdginducedm1lem1  27915  vtxdginducedm1lem4  27918  vtxdginducedm1  27919  vtxdginducedm1fi  27920  finsumvtxdg2ssteplem4  27924  rusgrnumwrdl2  27962  wksfval  27985  iswlkg  27989  wlkonprop  28035  wlkp1lem3  28052  wlkp1lem8  28057  wlkp1  28058  wksonproplem  28081  wksonproplemOLD  28082  wwlks  28209  wwlksnon  28225  wspthsnon  28226  clwwlk  28356  0wlkonlem2  28492  conngrv2edg  28568  eupthp1  28589  eupth2eucrct  28590  eupthvdres  28608  eupth2lem3  28609  eupth2lemb  28610  3cyclfrgrrn  28659  frgrwopreglem1  28685  frgrwopreg1  28691  imsmetlem  29061  dipfval  29073  sspval  29094  islno  29124  nmooval  29134  nmounbseqi  29148  nmobndseqi  29150  0ofval  29158  0oval  29159  ajfval  29180  isph  29193  phpar  29195  ajval  29232  ubthlem1  29241  ubthlem2  29242  minvecolem4b  29249  minvecolem4  29251  minvecolem5  29252  hlex  29269  ressplusf  31244  ressnm  31245  oppglt  31249  ressprs  31250  oduprs  31251  ismnt  31270  mgcval  31274  gsummptres  31321  gsummptres2  31322  gsumpart  31324  gsumhashmul  31325  inftmrel  31443  isinftm  31444  gsumvsca1  31488  ress1r  31495  rdivmuldivd  31497  ringinvval  31498  dvrcan5  31499  rmfsupp2  31501  ofldlt1  31521  resvsca  31538  quslmod  31563  islinds5  31572  ellspds  31573  elrsp  31578  linds2eq  31584  elringlsm  31590  lsmsnpridl  31595  grplsm0l  31600  qusima  31603  nsgmgc  31606  nsgqusf1o  31610  elrspunidl  31615  prmidl0  31635  idlsrgbas  31658  idlsrgplusg  31659  idlsrgmulr  31661  idlsrgtset  31662  rprmval  31673  fply1  31676  dimval  31695  dimvalfi  31696  lvecdim0  31699  mdetpmtr1  31782  rspectopn  31826  zarcls0  31827  zarcls  31833  zartopn  31834  zarmxt1  31839  rhmpreimacnlem  31843  rhmpreimacn  31844  pstmfval  31855  ordtrest2NEW  31882  ordtconnlem1  31883  fsumcvg4  31909  pl1cn  31914  qqhval  31933  sibf0  32310  sitgclg  32318  sitgaddlemb  32324  eulerpartlemgvv  32352  afsval  32660  pthhashvtx  33098  usgrcyclgt2v  33102  cusgr3cyclex  33107  acycgr2v  33121  cusgracyclt3v  33127  mrsubfval  33479  mrsubcv  33481  mrsubff  33483  mrsubrn  33484  elmrsubrn  33491  msubfval  33495  msubff  33501  mpstval  33506  elmpst  33507  msrval  33509  mstaval  33515  msubvrs  33531  mclsssvlem  33533  mclsval  33534  mclsind  33541  mppsval  33543  climlec3  33708  sdclem2  35909  sdclem1  35910  caures  35927  heiborlem3  35980  heibor  35988  grpokerinj  36060  rngoi  36066  dvrunz  36121  isdrngo1  36123  isdrngo2  36125  isrngohom  36132  idlval  36180  isidl  36181  0idl  36192  0rngo  36194  divrngidl  36195  smprngopr  36219  igenval  36228  lshpset  36999  lsatset  37011  lcvfbr  37041  islfl  37081  lfl0f  37090  lfl1  37091  lfladd0l  37095  lflnegl  37097  lflvscl  37098  lflvsdi1  37099  lflvsdi2  37100  lflvsdi2a  37101  lflvsass  37102  lfl0sc  37103  lflsc0N  37104  lfl1sc  37105  lkr0f  37115  lkrsc  37118  eqlkr2  37121  ldualvbase  37147  ldualfvadd  37149  ldualvaddval  37152  ldualsca  37153  ldualfvs  37157  ldualvsval  37159  isopos  37201  cmtfvalN  37231  cvrfval  37289  pats  37306  glbconN  37398  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  isline  37760  pointsetN  37762  psubspset  37765  ispsubsp  37766  pmapval  37778  paddfval  37818  paddval  37819  pclfvalN  37910  pclvalN  37911  polfvalN  37925  polvalN  37926  psubclsetN  37957  ispsubclN  37958  watvalN  38014  lhpset  38016  lautset  38103  islaut  38104  pautsetN  38119  ispautN  38120  ldilset  38130  ltrnset  38139  dilsetN  38174  cdleme26e  38380  cdleme26eALTN  38382  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32a  38462  cdleme40m  38488  cdleme40n  38489  cdleme42b  38499  tgrpbase  38767  tgrpopr  38768  istendo  38781  tendopl  38797  tendo02  38808  erngbase  38822  erngfplus  38823  erngfmul  38826  erngbase-rN  38830  erngfplus-rN  38831  erngfmul-rN  38834  cdlemk36  38934  cdlemkid  38957  dvasca  39027  dvavbase  39034  dvafvadd  39035  dvafvsca  39037  diafval  39052  diaval  39053  dvhsca  39103  dvhvbase  39108  dvhfvadd  39112  dvhfvsca  39121  docafvalN  39143  docavalN  39144  djafvalN  39155  djavalN  39156  dibfval  39162  dibopelvalN  39164  dibopelval2  39166  dibelval3  39168  diblsmopel  39192  dicfval  39196  dicval  39197  cdlemn11a  39228  dihvalcqpre  39256  dihopelvalcpre  39269  dihord6apre  39277  dihpN  39357  dochfval  39371  dochval  39372  djhfval  39418  djhval  39419  islpolN  39504  lpolconN  39508  dochpolN  39511  lcfrlem9  39571  lcd0vvalN  39634  mapdval  39649  mapd1o  39669  mapdunirnN  39671  mapdhval  39745  mapdhval0  39746  hvmapfval  39780  hvmapval  39781  hdmap1fval  39817  hdmap1vallem  39818  hgmapfval  39907  hlhilset  39955  hlhilbase  39957  hlhilplus  39958  hlhilvsca  39972  hlhilip  39973  hlhilnvl  39975  hlhillsm  39981  hlhillcs  39983  frlmfielbas  40238  frlm0vald  40269  evlsval3  40279  evlsbagval  40282  fsuppind  40286  fsuppssind  40289  mhpind  40290  mhphf  40292  islssfgi  40904  pwssplit4  40921  frlmpwfi  40930  mendplusgfval  41017  mendmulrfval  41019  mendvscafval  41022  idomrootle  41027  idomodle  41028  deg1mhm  41039  mnringelbased  41839  mnring0g2d  41845  mnringmulrd  41846  mnringmulrcld  41853  dvgrat  41937  uzmptshftfval  41971  climexp  43153  climinf  43154  climneg  43158  climdivf  43160  climconstmpt  43206  climresmpt  43207  climsubmpt  43208  fnlimfvre  43222  limsupvaluz  43256  limsupequzmpt2  43266  climuzlem  43291  climisp  43294  climxrrelem  43297  climxrre  43298  limsupgtlem  43325  liminflelimsupuz  43333  liminfgelimsupuz  43336  liminfequzmpt2  43339  liminfvaluz  43340  limsupvaluz3  43346  climliminflimsupd  43349  liminfreuzlem  43350  liminfltlem  43352  liminflimsupclim  43355  liminflbuz2  43363  liminfpnfuz  43364  xlimclim2lem  43387  climxlim2  43394  sge0isum  43972  sge0uzfsumgt  43989  sge0seq  43991  meaiunlelem  44013  caragendifcl  44059  omeiunle  44062  omeiunltfirp  44064  carageniuncl  44068  caragensal  44070  opnssborel  44180  smflimlem6  44321  smfpimcc  44352  smflimmpt  44354  smflimsuplem4  44367  smflimsuplem6  44369  smflimsuplem8  44371  smfliminflem  44374  isomuspgrlem2  45296  ushrisomgr  45304  upwlksfval  45308  isupwlkg  45310  ismgmhm  45348  issubmgm2  45355  submgmacs  45369  copisnmnd  45374  0ringdif  45439  rnghmval  45460  isrnghm  45461  c0snmgmhm  45483  c0snmhm  45484  zrrnghm  45486  zlidlring  45497  cznrng  45524  cznnring  45525  rngchomfvalALTV  45553  rngccofvalALTV  45556  rngccatidALTV  45558  ringchomfvalALTV  45616  ringccofvalALTV  45619  ringccatidALTV  45621  rngcrescrhm  45654  rngcrescrhmALTV  45672  ofaddmndmap  45690  suppmptcfin  45726  mptcfsupp  45727  dmatALTbas  45753  lcoop  45763  linccl  45766  lcosn0  45772  lincvalsc0  45773  lcoc0  45774  linc0scn0  45775  linc1  45777  lincscmcl  45784  islinindfis  45801  lincext1  45806  lincext2  45807  lindslinindimp2lem2  45811  lindslinindimp2lem3  45812  lindsrng01  45820  snlindsntorlem  45822  snlindsntor  45823  ldepspr  45825  lincresunit1  45829  lincresunit2  45830  lines  46088  line  46089  rrxlines  46090  sphere  46104  rrxsphere  46105  functhinclem1  46333  thincciso  46341
  Copyright terms: Public domain W3C validator