Theorem fvmpt 6947

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)

Hypotheses

Ref	Expression
fvmptg.1	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptg.2	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmpt.3	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
fvmpt	⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt

Step	Hyp	Ref	Expression
1		fvmpt.3	. 2 ⊢ 𝐶 ∈ V
2		fvmptg.1	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3		fvmptg.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
4	2, 3	fvmptg 6945	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V) → (𝐹‘𝐴) = 𝐶)
5	1, 4	mpan2 692	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ↦ cmpt 5166  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fvmptex  6962  fvmptrabfv  6980  mptfvmpt  7183  fvmptopab  7422  ofval  7642  caofinvl  7663  fvresex  7913  1stval  7944  2ndval  7945  reldm  7997  curry1val  8055  curry2val  8059  fsplitfpar  8068  fnwelem  8081  brtpos2  8182  onovuni  8282  tz7.44-1  8345  oasuc  8459  oesuclem  8460  omsuc  8461  onasuc  8463  onmsuc  8464  fsetfocdm  8808  fvmptmap  8829  xpcomco  9005  unxpdomlem1  9166  unfilem2  9216  ordtypelem3  9435  ixpiunwdom  9505  inf3lema  9545  noinfep  9581  cantnfval  9589  cantnflem1d  9609  cantnflem1  9610  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  r1sucg  9693  r0weon  9934  infxpenc2lem1  9941  fseqenlem1  9946  fseqenlem2  9947  dfac8alem  9951  ac5num  9958  acni2  9968  dfac4  10044  dfac2a  10052  dfacacn  10064  dfac12lem1  10066  ackbij1lem7  10147  ackbij2lem2  10161  ackbij2lem3  10162  cfsmolem  10192  fin23lem28  10262  fin23lem39  10272  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  fin1a2lem3  10324  itunifval  10338  itunisuc  10341  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  zorn2lem1  10418  negiso  12136  infrenegsup  12139  uzval  12790  flval  13753  ceilval  13797  ceilval2  13799  monoord2  13995  seqf1olem2  14004  seqf1o  14005  seqdistr  14015  serle  14019  seqof  14021  swrdfv  14611  revval  14722  revfv  14725  wwlktovf1  14919  wwlktovfo  14920  sgnval  15050  cjval  15064  reval  15068  imval  15069  sqrtval  15199  absval  15200  limsupval  15436  limsupgval  15438  climmpt  15533  climle  15602  rlimdiv  15608  isercolllem1  15627  isercoll2  15631  caurcvg2  15640  fsumser  15692  isumadd  15729  fsumcnv  15735  fsumrev  15741  fsumshft  15742  iserabs  15778  cvgcmp  15779  cvgcmpce  15781  incexclem  15801  isumless  15810  divcnvshft  15820  supcvg  15821  harmonic  15824  trireciplem  15827  trirecip  15828  expcnv  15829  explecnv  15830  geolim  15835  geolim2  15836  geo2lim  15840  geomulcvg  15841  geoisum  15842  geoisumr  15843  geoisum1  15844  geoisum1c  15845  cvgrat  15848  mertenslem2  15850  mertens  15851  prodfdiv  15861  fprodser  15914  fprodshft  15941  fprodrev  15942  fprodcnv  15948  iprodmul  15968  bpolylem  16013  eftval  16041  efval  16044  efcvgfsum  16051  ege2le3  16055  eftlub  16076  eflegeo  16088  sinval  16089  cosval  16090  tanval  16095  eirrlem  16171  rpnnen2lem1  16181  rpnnen2lem2  16182  bitsfval  16392  bitsinv2  16412  bitsinv  16417  sadcf  16422  sadc0  16423  sadcp1  16424  smupf  16447  smup0  16448  smupp1  16449  qnumval  16707  qdenval  16708  phival  16737  crth  16748  phimullem  16749  eulerthlem2  16752  phisum  16761  odzval  16762  iserodd  16806  pcmpt  16863  prmreclem1  16887  prmreclem2  16888  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  1arithlem1  16894  1arithlem2  16895  vdwapfval  16942  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  ramub1lem2  16998  ramcl  17000  prmoval  17004  strfvnd  17155  topnval  17397  prdsplusgfval  17437  prdsmulrfval  17439  isacs  17617  acsfn  17625  homffval  17656  comfffval  17664  oppcval  17679  monfval  17699  oppcmon  17705  sectffval  17717  invffval  17725  isoval  17732  idfuval  17843  homafval  17996  arwval  18010  coafval  18031  yonedainv  18247  oduval  18254  pltfval  18295  lubfval  18314  lubval  18320  glbfval  18327  glbval  18333  p0val  18391  p1val  18392  ipoval  18496  plusffval  18614  grpidval  18629  issubmgm  18670  issubm  18771  prdspjmhm  18797  efmnd  18838  smndex1gbas  18870  smndex1gid  18872  smndex1igid  18874  smndex1igidOLD  18875  grpinvfval  18954  grpinvval  18956  grpsubfval  18959  grpsubfvalALT  18960  grplactval  19018  prdsinvlem  19025  mulgfval  19045  mulgfvalALT  19046  pwsmulg  19095  issubg  19102  isnsg  19130  cycsubmel  19175  cycsubgcl  19181  conjghm  19224  conjnmz  19227  cntrval  19294  cntzfval  19295  cntzval  19296  oppgval  19322  psgnfval  19475  psgnval  19482  odfval  19507  odval  19509  sylow1lem4  19576  pgpssslw  19589  sylow2blem3  19597  sylow3lem2  19603  lsmfval  19613  pj1fval  19669  efgval  19692  efgsval  19706  frgpval  19733  vrgpval  19742  mulgmhm  19802  mulgghm  19803  ablfaclem1  20062  mgpval  20124  srglmhm  20202  srgrmhm  20203  ringlghm  20293  ringrghm  20294  pwspjmhmmgpd  20307  pwsexpg  20308  opprval  20318  dvdsrval  20341  isunit  20353  invrfval  20369  dvrfval  20382  isirred  20399  issubrng  20524  issubrg  20548  rgspnval  20589  rrgval  20674  fidomndrnglem  20749  issdrg  20765  abvfval  20787  abvtrivd  20809  staffval  20818  stafval  20819  scaffval  20875  lmodvsghm  20918  lssset  20928  lspfval  20968  islbs  21071  sraval  21170  rlmval  21186  2idlval  21249  lpival  21322  expmhm  21416  expghm  21455  mulgghm2  21456  mulgrhm  21457  zrhval  21487  zrhmulg  21489  zlmval  21495  chrval  21503  znval  21515  znzrhval  21526  evpmss  21566  psgnevpmb  21567  ip0l  21616  ipffval  21628  ocvfval  21646  ocvval  21647  cssval  21662  thlval  21675  pjfval  21686  pjval  21690  isobs  21700  prdsinvgd2  21722  uvcresum  21773  frlmup1  21778  frlmup2  21779  islinds  21789  islindf5  21819  aspval  21852  asclval  21859  psrmulval  21923  psrlidm  21940  psrridm  21941  psrascl  21957  mvrval  21960  mvrval2  21961  mplmonmul  22014  evlslem3  22058  evlslem1  22060  evlsval  22064  evlssca  22072  evlsvar  22073  psdmul  22132  psdmvr  22135  psr1val  22149  vr1val  22155  ply1val  22157  coe1fval  22169  coe1fv  22170  coe1tmmul2  22241  coe1tmmul  22242  coe1tmmul2fv  22243  coe1pwmulfv  22245  evls1val  22285  evl1fval  22293  evl1val  22294  mamulid  22406  mamurid  22407  mdetleib  22552  mdetleib1  22556  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  cpmidpmatlem1  22835  ordtval  23154  cnpval  23201  ptpjpre1  23536  ptpjopn  23577  dfac14  23583  upxp  23588  uptx  23590  hauseqlcld  23611  txlm  23613  xkoptsub  23619  xkoinjcn  23652  kqval  23691  xpstopnlem1  23774  fmval  23908  flfval  23955  ptcmplem2  24018  ptcmplem3  24019  symgtgp  24071  qustgpopn  24085  ussval  24224  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  mopnval  24403  prdsxmslem2  24494  nmfval  24553  nmval  24554  nmoval  24680  metdsval  24813  divcn  24835  mulc1cncf  24872  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  cnheiborlem  24921  evth  24926  evth2  24927  lebnumlem3  24930  isphtpy  24948  isphtpc  24961  pcofval  24977  pcovalg  24979  pco1  24982  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevcl  24992  pcorevlem  24993  pcorev2  24995  pi1xfrcnv  25024  cphnm  25160  tcphval  25185  tcphnmval  25196  cfilfval  25231  iscmet  25251  iscmet3lem3  25257  rrxval  25354  ehlval  25381  ivth2  25422  ovolval  25440  ovollb2lem  25455  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliunlem2  25470  ovolicc1  25483  voliunlem1  25517  voliunlem2  25518  voliunlem3  25519  volsup  25523  ioorval  25541  uniioombllem3  25552  uniioombllem6  25555  volsup2  25572  volcn  25573  volivth  25574  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  vitali  25580  mbfmax  25616  mbfimaopnlem  25622  itg1val  25650  i1f1lem  25656  itg11  25658  itg1addlem4  25666  itg1mulc  25671  i1fres  25672  itg1climres  25681  mbfi1fseqlem2  25683  mbfi1fseqlem3  25684  mbfi1fseqlem6  25687  mbfi1flimlem  25689  mbfi1flim  25690  mbfmullem2  25691  itg2seq  25709  itg2uba  25710  itg2splitlem  25715  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  itg2cnlem1  25728  itg2cn  25730  limccnp2  25859  dvnff  25890  dvnp1  25892  cpnfval  25899  elcpn  25901  dvrec  25922  dvcnvlem  25943  dveflem  25946  dvef  25947  dvferm1  25952  dvferm2  25954  rolle  25957  dvlip  25960  dvlipcn  25961  dv11cn  25968  dvivthlem1  25975  dvivth  25977  lhop1lem  25980  ftc1lem1  26002  ftc1lem5  26007  ftc2  26011  itgsubstlem  26015  tdeglem3  26024  tdeglem4  26025  mdegval  26028  mdegmullem  26043  deg1fval  26045  deg1ldg  26057  deg1leb  26060  coe1mul3  26064  uc1pval  26105  mon1pval  26107  mon1pid  26119  q1pval  26120  r1pval  26123  ply1remlem  26130  ig1pval  26141  plyval  26158  elply2  26161  plyeq0lem  26175  coeval  26188  dgrval  26193  coeid2  26204  coemullem  26215  coemul  26217  elqaalem1  26285  elqaalem2  26286  elqaalem3  26287  iaa  26291  aareccl  26292  aannenlem1  26294  geolim3  26305  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  aaliou3  26317  tayl0  26327  taylthlem1  26338  taylthlem2  26339  ulmshftlem  26354  ulmshft  26355  ulmuni  26357  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  mbfulm  26371  iblulm  26372  itgulm  26373  pserval  26375  pserval2  26376  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  pserulm  26387  pserdvlem2  26393  pserdv  26394  abelthlem1  26396  abelthlem3  26398  abelthlem4  26399  abelthlem5  26400  abelthlem6  26401  abelthlem7  26403  abelthlem8  26404  abelthlem9  26405  resinf1o  26500  efif1olem4  26509  eff1olem  26512  logcnlem5  26610  logtayllem  26623  logtayl  26624  logtaylsum  26625  logtayl2  26626  logccv  26627  asinval  26846  acosval  26847  atanval  26848  atantayl  26901  leibpilem2  26905  leibpi  26906  leibpisum  26907  log2cnv  26908  log2tlbnd  26909  areaval  26928  efrlim  26933  dfef2  26934  amgmlem  26953  emcllem2  26960  emcllem3  26961  emcllem4  26962  emcllem5  26963  emcllem6  26964  emcllem7  26965  zetacvg  26978  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulm2  26999  lgamcvglem  27003  igamval  27010  lgamcvg2  27018  gamcvg2lem  27022  ftalem7  27042  basellem2  27045  basellem3  27046  basellem4  27047  basellem5  27048  basellem6  27049  basellem8  27051  basellem9  27052  chtval  27073  vmaval  27076  chpval  27085  ppival  27090  muval  27095  prmorcht  27141  sqff1o  27145  dvdsflsumcom  27151  musum  27154  muinv  27156  sgmppw  27160  fsumvma  27176  pclogsum  27178  dchrfi  27218  bposlem5  27251  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgsfval  27265  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgsqrlem2  27310  lgsqrlem4  27312  lgseisenlem2  27339  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasumiflem1  27464  dchrvmaeq0  27467  dchrisum0fval  27468  dchrisum0re  27476  mulog2sumlem1  27497  pntrval  27525  pntsval  27535  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntlem3  27572  abvcxp  27578  padicfval  27579  padicval  27580  padicabv  27593  ostth1  27596  ostth2  27600  ostth3  27601  nosupfv  27670  noinffv  27685  newval  27827  leftval  27841  rightval  27842  iscgrg  28580  legval  28652  ishpg  28827  iscgra  28877  isinag  28906  isleag  28915  iseqlg  28935  ttgval  28943  elee  28962  axsegconlem1  28986  axsegconlem9  28994  axsegconlem10  28995  axpasch  29010  axlowdimlem15  29025  axlowdim  29030  axeuclidlem  29031  axcontlem2  29034  eengv  29048  vtxval  29069  iedgval  29070  edgval  29118  vtxdgval  29537  wwlksnextinj  29967  wwlksnextsurj  29968  clwwlkfv  30118  clwwlknonmpo  30159  fusgreg2wsplem  30403  fusgreghash2wsp  30408  numclwwlk1lem2fv  30426  gidval  30583  grpoinvval  30594  bafval  30675  imsval  30756  dipfval  30773  sspval  30794  nmooval  30834  hmoval  30881  ipasslem8  30908  ipasslem9  30909  ipblnfi  30926  ubthlem2  30942  htthlem  30988  normval  31195  ocval  31351  occllem  31374  hsupval  31405  pjhfval  31467  pjhval  31468  chscllem2  31709  chscllem3  31710  hosval  31811  homval  31812  hodval  31813  hfsval  31814  hfmval  31815  brafval  32014  braval  32015  kbval  32025  eigvalval  32031  cnlnadjlem1  32138  nmopadjlei  32159  hmopidmchi  32222  strlem2  32322  hstrlem2  32330  cdj3lem2  32506  ofpreima  32738  psgnfzto1stlem  33161  evpmval  33206  altgnsg  33210  inftmrel  33241  isinftm  33242  qusker  33409  qusvscpbl  33411  qusvsval  33412  mxidlval  33521  idlsrgval  33563  psrmonmul  33694  dimval  33745  dimvalfi  33746  smatfval  33939  lmatval  33957  locfinreflem  33984  rspecval  34008  rmulccn  34072  xrmulc1cn  34074  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  xrge0iif1  34082  qqhval  34116  rrhval  34140  xrhval  34162  ddeval1  34378  ddeval0  34379  sxbrsigalem0  34415  sxbrsigalem3  34416  eulerpartlemgv  34517  rrvmbfm  34586  dstrvval  34615  coinflippv  34628  ballotlem2  34633  ballotlemfval  34634  ballotlemi  34645  ballotlemsval  34653  ballotlemrval  34662  ballotth  34682  plymulx  34692  signstfv  34707  signsvvfval  34722  onvf1odlem3  35287  derangval  35349  subfacval  35355  erdszelem3  35375  erdszelem9  35381  erdszelem10  35382  txpconn  35414  indispconn  35416  cvxpconn  35424  cvmlift2lem2  35486  cvmlift2lem3  35487  cvmlift2lem7  35491  cvmliftphtlem  35499  cvmlift3lem4  35504  snmlfval  35512  snmlval  35513  gonafv  35532  mvtval  35682  mrsubffval  35689  mrsubcv  35692  mrsubrn  35695  elmrsubrn  35702  msubffval  35705  mvhval  35716  mpstval  35717  mstaval  35726  mclsval  35745  mppsval  35754  sinccvglem  35854  circum  35856  divcnvlin  35915  iprodefisum  35923  iprodgam  35924  faclimlem1  35925  faclimlem2  35926  faclim  35928  iprodfac  35929  faclim2  35930  dfrdg2  35975  findabrcl  36636  dnival  36731  bj-evalval  37387  bj-inftyexpitaudisj  37519  bj-inftyexpiinv  37522  bj-inftyexpidisj  37524  curfv  37921  finixpnum  37926  poimirlem16  37957  poimir  37974  broucube  37975  mblfinlem2  37979  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  itg2addnclem3  37994  ftc1cnnc  38013  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  ftc2nc  38023  fvopabf4g  38043  sdclem2  38063  fdc  38066  lmclim2  38079  geomcau  38080  istotbnd  38090  isbnd  38101  prdsbnd2  38116  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  rrnval  38148  rrncmslem  38153  idlval  38334  pridlval  38354  maxidlval  38360  lshpset  39424  lsatset  39436  lcvfbr  39466  lflset  39505  lflnegcl  39521  lshpkrlem1  39556  lshpkrlem2  39557  lshpkrlem3  39558  ldualset  39571  cmtfvalN  39656  cvrfval  39714  pats  39731  llnset  39951  lplnset  39975  lvolset  40018  lineset  40184  pointsetN  40187  psubspset  40190  pmapval  40203  paddfval  40243  pclfvalN  40335  polfvalN  40350  polvalN  40351  psubclsetN  40382  watvalN  40439  lhpset  40441  lautset  40528  pautsetN  40544  ldilset  40555  ltrnset  40564  dilsetN  40599  trnsetN  40602  trlset  40607  trlval  40608  tgrpset  41191  tendoset  41205  tendo02  41233  erngset  41246  erngset-rN  41254  cdlemksv  41290  dvaset  41451  dvaplusgv  41456  diafval  41477  diaval  41478  dvhset  41527  cdlemm10N  41564  docafvalN  41568  djafvalN  41580  dibfval  41587  dibval  41588  dicfval  41621  dicval  41622  dihval  41678  dochfval  41796  djhfval  41843  dochfl1  41922  lpolsetN  41928  lcdval  42035  mapdhval  42170  hvmapfval  42205  hdmap1fval  42242  fimgmcyc  42979  prjspval  43036  isnacs  43136  mzpclval  43157  mzpsubst  43180  mzprename  43181  mzpcompact2lem  43183  eldiophb  43189  diophrw  43191  eldioph2  43194  diophin  43204  diophun  43205  diophren  43241  pell1qrval  43274  pell14qrval  43276  pell1234qrval  43278  pellfundval  43308  rmxypairf1o  43339  rmxyval  43343  mzpcong  43400  pw2f1ocnv  43465  dnnumch1  43472  dfac11  43490  hbtlem1  43551  hbtlem7  43553  elmnc  43564  dgraaval  43572  mpaaval  43579  itgoval  43589  flcidc  43598  mendval  43607  cytpval  43630  cantnfub  43749  cantnfresb  43752  tfsconcatrev  43776  elcnvlem  44028  comptiunov2i  44133  dftrcl3  44147  trclfvcom  44150  cnvtrclfv  44151  cotrcltrcl  44152  trclimalb2  44153  trclfvdecomr  44155  dfrtrcl3  44160  dfrtrcl4  44165  clsk1indlem0  44468  clsk1indlem2  44469  clsk1indlem3  44470  clsk1indlem4  44471  clsk1indlem1  44472  k0004val  44577  lhe4.4ex1a  44756  addrfv  44895  subrfv  44896  mulvfv  44897  monoord2xrv  45911  sumnnodd  46060  liminfgval  46190  ioodvbdlimc2lem  46362  itgsin0pilem1  46378  stoweidlem55  46483  wallispilem1  46493  wallispilem2  46494  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  dirkerval  46519  fourierdlem2  46537  fourierdlem3  46538  fourierdlem29  46564  fourierdlem62  46596  fourierdlem80  46614  fourierdlem103  46637  fourierdlem104  46638  fourierswlem  46658  fouriersw  46659  iundjiunlem  46887  carageniuncllem2  46950  0ome  46957  hoidmv1le  47022  hoidmvlelem3  47025  smflimsuplem7  47254  nthrucw  47316  iccpval  47875  fppr  48202  bigoval  49025  ackval0  49156  ackval41a  49170  eenglngeehlnm  49215  oppcinito  49710  oppctermo  49711  dfinito4  49976  prstcval  50026  mndtcval  50054  setc1onsubc  50077  lmdfval2  50130  cmdfval2  50131  vsetrec  50178  onsetreclem1  50180  elpglem3  50188  pgindnf  50191  sinhval-named  50211  coshval-named  50212  tanhval-named  50213  secval  50222  cscval  50223  cotval  50224  aacllem  50276