Theorem fvmpt 6949

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 6947	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V) → (𝐹‘𝐴) = 𝐶)
5	1, 4	mpan2 692	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ↦ cmpt 5181  ‘cfv 6500

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 2709  ax-sep 5243  ax-pr 5379

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  fvmptex  6964  fvmptrabfv  6982  mptfvmpt  7184  fvmptopab  7423  ofval  7643  caofinvl  7664  fvresex  7914  1stval  7945  2ndval  7946  reldm  7998  curry1val  8057  curry2val  8061  fsplitfpar  8070  fnwelem  8083  brtpos2  8184  onovuni  8284  tz7.44-1  8347  oasuc  8461  oesuclem  8462  omsuc  8463  onasuc  8465  onmsuc  8466  fsetfocdm  8810  fvmptmap  8831  xpcomco  9007  unxpdomlem1  9168  unfilem2  9218  ordtypelem3  9437  ixpiunwdom  9507  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  12134  infrenegsup  12137  uzval  12765  flval  13726  ceilval  13770  ceilval2  13772  monoord2  13968  seqf1olem2  13977  seqf1o  13978  seqdistr  13988  serle  13992  seqof  13994  swrdfv  14584  revval  14695  revfv  14698  wwlktovf1  14892  wwlktovfo  14893  sgnval  15023  cjval  15037  reval  15041  imval  15042  sqrtval  15172  absval  15173  limsupval  15409  limsupgval  15411  climmpt  15506  climle  15575  rlimdiv  15581  isercolllem1  15600  isercoll2  15604  caurcvg2  15613  fsumser  15665  isumadd  15702  fsumcnv  15708  fsumrev  15714  fsumshft  15715  iserabs  15750  cvgcmp  15751  cvgcmpce  15753  incexclem  15771  isumless  15780  divcnvshft  15790  supcvg  15791  harmonic  15794  trireciplem  15797  trirecip  15798  expcnv  15799  explecnv  15800  geolim  15805  geolim2  15806  geo2lim  15810  geomulcvg  15811  geoisum  15812  geoisumr  15813  geoisum1  15814  geoisum1c  15815  cvgrat  15818  mertenslem2  15820  mertens  15821  prodfdiv  15831  fprodser  15884  fprodshft  15911  fprodrev  15912  fprodcnv  15918  iprodmul  15938  bpolylem  15983  eftval  16011  efval  16014  efcvgfsum  16021  ege2le3  16025  eftlub  16046  eflegeo  16058  sinval  16059  cosval  16060  tanval  16065  eirrlem  16141  rpnnen2lem1  16151  rpnnen2lem2  16152  bitsfval  16362  bitsinv2  16382  bitsinv  16387  sadcf  16392  sadc0  16393  sadcp1  16394  smupf  16417  smup0  16418  smupp1  16419  qnumval  16676  qdenval  16677  phival  16706  crth  16717  phimullem  16718  eulerthlem2  16721  phisum  16730  odzval  16731  iserodd  16775  pcmpt  16832  prmreclem1  16856  prmreclem2  16857  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  1arithlem1  16863  1arithlem2  16864  vdwapfval  16911  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  ramub1lem2  16967  ramcl  16969  prmoval  16973  strfvnd  17124  topnval  17366  prdsplusgfval  17406  prdsmulrfval  17408  isacs  17586  acsfn  17594  homffval  17625  comfffval  17633  oppcval  17648  monfval  17668  oppcmon  17674  sectffval  17686  invffval  17694  isoval  17701  idfuval  17812  homafval  17965  arwval  17979  coafval  18000  yonedainv  18216  oduval  18223  pltfval  18264  lubfval  18283  lubval  18289  glbfval  18296  glbval  18302  p0val  18360  p1val  18361  ipoval  18465  plusffval  18583  grpidval  18598  issubmgm  18639  issubm  18740  prdspjmhm  18766  efmnd  18807  smndex1igid  18841  grpinvfval  18920  grpinvval  18922  grpsubfval  18925  grpsubfvalALT  18926  grplactval  18984  prdsinvlem  18991  mulgfval  19011  mulgfvalALT  19012  pwsmulg  19061  issubg  19068  isnsg  19096  cycsubmel  19141  cycsubgcl  19147  conjghm  19190  conjnmz  19193  cntrval  19260  cntzfval  19261  cntzval  19262  oppgval  19288  psgnfval  19441  psgnval  19448  odfval  19473  odval  19475  sylow1lem4  19542  pgpssslw  19555  sylow2blem3  19563  sylow3lem2  19569  lsmfval  19579  pj1fval  19635  efgval  19658  efgsval  19672  frgpval  19699  vrgpval  19708  mulgmhm  19768  mulgghm  19769  ablfaclem1  20028  mgpval  20090  srglmhm  20168  srgrmhm  20169  ringlghm  20259  ringrghm  20260  pwspjmhmmgpd  20275  pwsexpg  20276  opprval  20286  dvdsrval  20309  isunit  20321  invrfval  20337  dvrfval  20350  isirred  20367  issubrng  20492  issubrg  20516  rgspnval  20557  rrgval  20642  fidomndrnglem  20717  issdrg  20733  abvfval  20755  abvtrivd  20777  staffval  20786  stafval  20787  scaffval  20843  lmodvsghm  20886  lssset  20896  lspfval  20936  islbs  21040  sraval  21139  rlmval  21155  2idlval  21218  lpival  21291  expmhm  21403  expghm  21442  mulgghm2  21443  mulgrhm  21444  zrhval  21474  zrhmulg  21476  zlmval  21482  chrval  21490  znval  21502  znzrhval  21513  evpmss  21553  psgnevpmb  21554  ip0l  21603  ipffval  21615  ocvfval  21633  ocvval  21634  cssval  21649  thlval  21662  pjfval  21673  pjval  21677  isobs  21687  prdsinvgd2  21709  uvcresum  21760  frlmup1  21765  frlmup2  21766  islinds  21776  islindf5  21806  aspval  21840  asclval  21847  psrmulval  21912  psrlidm  21929  psrridm  21930  psrascl  21946  mvrval  21949  mvrval2  21950  mplmonmul  22003  evlslem3  22047  evlslem1  22049  evlsval  22053  evlssca  22061  evlsvar  22062  psdmul  22121  psdmvr  22124  psr1val  22138  vr1val  22144  ply1val  22146  coe1fval  22158  coe1fv  22159  coe1tmmul2  22230  coe1tmmul  22231  coe1tmmul2fv  22232  coe1pwmulfv  22234  evls1val  22276  evl1fval  22284  evl1val  22285  mamulid  22397  mamurid  22398  mdetleib  22543  mdetleib1  22547  mdetunilem9  22576  mdetuni0  22577  mdetmul  22579  cpmidpmatlem1  22826  ordtval  23145  cnpval  23192  ptpjpre1  23527  ptpjopn  23568  dfac14  23574  upxp  23579  uptx  23581  hauseqlcld  23602  txlm  23604  xkoptsub  23610  xkoinjcn  23643  kqval  23682  xpstopnlem1  23765  fmval  23899  flfval  23946  ptcmplem2  24009  ptcmplem3  24010  symgtgp  24062  qustgpopn  24076  ussval  24215  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  mopnval  24394  prdsxmslem2  24485  nmfval  24544  nmval  24545  nmoval  24671  metdsval  24804  divcnOLD  24825  divcn  24827  mulc1cncf  24866  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  cnheiborlem  24921  evth  24926  evth2  24927  lebnumlem3  24930  isphtpy  24948  isphtpc  24961  pcofval  24978  pcovalg  24980  pco1  24983  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevcl  24993  pcorevlem  24994  pcorev2  24996  pi1xfrcnv  25025  cphnm  25161  tcphval  25186  tcphnmval  25197  cfilfval  25232  iscmet  25252  iscmet3lem3  25258  rrxval  25355  ehlval  25382  ivth2  25424  ovolval  25442  ovollb2lem  25457  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem2  25472  ovolicc1  25485  voliunlem1  25519  voliunlem2  25520  voliunlem3  25521  volsup  25525  ioorval  25543  uniioombllem3  25554  uniioombllem6  25557  volsup2  25574  volcn  25575  volivth  25576  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  vitali  25582  mbfmax  25618  mbfimaopnlem  25624  itg1val  25652  i1f1lem  25658  itg11  25660  itg1addlem4  25668  itg1mulc  25673  i1fres  25674  itg1climres  25683  mbfi1fseqlem2  25685  mbfi1fseqlem3  25686  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfi1flim  25692  mbfmullem2  25693  itg2seq  25711  itg2uba  25712  itg2splitlem  25717  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  itg2cnlem1  25730  itg2cn  25732  limccnp2  25861  dvnff  25893  dvnp1  25895  cpnfval  25902  elcpn  25904  dvrec  25927  dvcnvlem  25948  dveflem  25951  dvef  25952  dvferm1  25957  dvferm2  25959  rolle  25962  dvlip  25966  dvlipcn  25967  dv11cn  25974  dvivthlem1  25981  dvivth  25983  lhop1lem  25986  ftc1lem1  26010  ftc1lem5  26015  ftc2  26019  itgsubstlem  26023  tdeglem3  26032  tdeglem4  26033  mdegval  26036  mdegmullem  26051  deg1fval  26053  deg1ldg  26065  deg1leb  26068  coe1mul3  26072  uc1pval  26113  mon1pval  26115  mon1pid  26127  q1pval  26128  r1pval  26131  ply1remlem  26138  ig1pval  26149  plyval  26166  elply2  26169  plyeq0lem  26183  coeval  26196  dgrval  26201  coeid2  26212  coemullem  26223  coemul  26225  elqaalem1  26295  elqaalem2  26296  elqaalem3  26297  iaa  26301  aareccl  26302  aannenlem1  26304  geolim3  26315  aaliou3lem1  26318  aaliou3lem2  26319  aaliou3lem5  26323  aaliou3lem6  26324  aaliou3lem7  26325  aaliou3  26327  tayl0  26337  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmshftlem  26366  ulmshft  26367  ulmuni  26369  ulmcau  26372  ulmdvlem1  26377  ulmdvlem3  26379  mtest  26381  mtestbdd  26382  mbfulm  26383  iblulm  26384  itgulm  26385  pserval  26387  pserval2  26388  radcnvlem1  26390  radcnvlem2  26391  dvradcnv  26398  pserulm  26399  pserdvlem2  26406  pserdv  26407  abelthlem1  26409  abelthlem3  26411  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  resinf1o  26513  efif1olem4  26522  eff1olem  26525  logcnlem5  26623  logtayllem  26636  logtayl  26637  logtaylsum  26638  logtayl2  26639  logccv  26640  asinval  26860  acosval  26861  atanval  26862  atantayl  26915  leibpilem2  26919  leibpi  26920  leibpisum  26921  log2cnv  26922  log2tlbnd  26923  areaval  26942  efrlim  26947  efrlimOLD  26948  dfef2  26949  amgmlem  26968  emcllem2  26975  emcllem3  26976  emcllem4  26977  emcllem5  26978  emcllem6  26979  emcllem7  26980  zetacvg  26993  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulm2  27014  lgamcvglem  27018  igamval  27025  lgamcvg2  27033  gamcvg2lem  27037  ftalem7  27057  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  basellem6  27064  basellem8  27066  basellem9  27067  chtval  27088  vmaval  27091  chpval  27100  ppival  27105  muval  27110  prmorcht  27156  sqff1o  27160  dvdsflsumcom  27166  musum  27169  muinv  27171  sgmppw  27176  fsumvma  27192  pclogsum  27194  dchrfi  27234  bposlem5  27267  bposlem7  27269  bposlem8  27270  bposlem9  27271  lgsfval  27281  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  lgsqrlem2  27326  lgsqrlem4  27328  lgseisenlem2  27355  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasumiflem1  27480  dchrvmaeq0  27483  dchrisum0fval  27484  dchrisum0re  27492  mulog2sumlem1  27513  pntrval  27541  pntsval  27551  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntlem3  27588  abvcxp  27594  padicfval  27595  padicval  27596  padicabv  27609  ostth1  27612  ostth2  27616  ostth3  27617  nosupfv  27686  noinffv  27701  newval  27843  leftval  27857  rightval  27858  iscgrg  28596  legval  28668  ishpg  28843  iscgra  28893  isinag  28922  isleag  28931  iseqlg  28951  ttgval  28959  elee  28978  axsegconlem1  29002  axsegconlem9  29010  axsegconlem10  29011  axpasch  29026  axlowdimlem15  29041  axlowdim  29046  axeuclidlem  29047  axcontlem2  29050  eengv  29064  vtxval  29085  iedgval  29086  edgval  29134  vtxdgval  29554  wwlksnextinj  29984  wwlksnextsurj  29985  clwwlkfv  30135  clwwlknonmpo  30176  fusgreg2wsplem  30420  fusgreghash2wsp  30425  numclwwlk1lem2fv  30443  gidval  30600  grpoinvval  30611  bafval  30692  imsval  30773  dipfval  30790  sspval  30811  nmooval  30851  hmoval  30898  ipasslem8  30925  ipasslem9  30926  ipblnfi  30943  ubthlem2  30959  htthlem  31005  normval  31212  ocval  31368  occllem  31391  hsupval  31422  pjhfval  31484  pjhval  31485  chscllem2  31726  chscllem3  31727  hosval  31828  homval  31829  hodval  31830  hfsval  31831  hfmval  31832  brafval  32031  braval  32032  kbval  32042  eigvalval  32048  cnlnadjlem1  32155  nmopadjlei  32176  hmopidmchi  32239  strlem2  32339  hstrlem2  32347  cdj3lem2  32523  ofpreima  32755  psgnfzto1stlem  33194  evpmval  33239  altgnsg  33243  inftmrel  33274  isinftm  33275  qusker  33442  qusvscpbl  33444  qusvsval  33445  mxidlval  33554  idlsrgval  33596  psrmonmul  33727  dimval  33778  dimvalfi  33779  smatfval  33973  lmatval  33991  locfinreflem  34018  rspecval  34042  rmulccn  34106  xrmulc1cn  34108  xrge0iifcv  34112  xrge0iifiso  34113  xrge0iifhom  34115  xrge0iif1  34116  qqhval  34150  rrhval  34174  xrhval  34196  ddeval1  34412  ddeval0  34413  sxbrsigalem0  34449  sxbrsigalem3  34450  eulerpartlemgv  34551  rrvmbfm  34620  dstrvval  34649  coinflippv  34662  ballotlem2  34667  ballotlemfval  34668  ballotlemi  34679  ballotlemsval  34687  ballotlemrval  34696  ballotth  34716  plymulx  34726  signstfv  34741  signsvvfval  34756  onvf1odlem3  35321  derangval  35383  subfacval  35389  erdszelem3  35409  erdszelem9  35415  erdszelem10  35416  txpconn  35448  indispconn  35450  cvxpconn  35458  cvmlift2lem2  35520  cvmlift2lem3  35521  cvmlift2lem7  35525  cvmliftphtlem  35533  cvmlift3lem4  35538  snmlfval  35546  snmlval  35547  gonafv  35566  mvtval  35716  mrsubffval  35723  mrsubcv  35726  mrsubrn  35729  elmrsubrn  35736  msubffval  35739  mvhval  35750  mpstval  35751  mstaval  35760  mclsval  35779  mppsval  35788  sinccvglem  35888  circum  35890  divcnvlin  35949  iprodefisum  35957  iprodgam  35958  faclimlem1  35959  faclimlem2  35960  faclim  35962  iprodfac  35963  faclim2  35964  dfrdg2  36009  findabrcl  36670  dnival  36693  bj-evalval  37328  bj-inftyexpitaudisj  37460  bj-inftyexpiinv  37463  bj-inftyexpidisj  37465  curfv  37851  finixpnum  37856  poimirlem16  37887  poimir  37904  broucube  37905  mblfinlem2  37909  voliunnfl  37915  volsupnfl  37916  itg2addnclem  37922  itg2addnclem3  37924  ftc1cnnc  37943  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anc  37952  ftc2nc  37953  fvopabf4g  37973  sdclem2  37993  fdc  37996  lmclim2  38009  geomcau  38010  istotbnd  38020  isbnd  38031  prdsbnd2  38046  heiborlem6  38067  heiborlem7  38068  heiborlem8  38069  rrnval  38078  rrncmslem  38083  idlval  38264  pridlval  38284  maxidlval  38290  lshpset  39354  lsatset  39366  lcvfbr  39396  lflset  39435  lflnegcl  39451  lshpkrlem1  39486  lshpkrlem2  39487  lshpkrlem3  39488  ldualset  39501  cmtfvalN  39586  cvrfval  39644  pats  39661  llnset  39881  lplnset  39905  lvolset  39948  lineset  40114  pointsetN  40117  psubspset  40120  pmapval  40133  paddfval  40173  pclfvalN  40265  polfvalN  40280  polvalN  40281  psubclsetN  40312  watvalN  40369  lhpset  40371  lautset  40458  pautsetN  40474  ldilset  40485  ltrnset  40494  dilsetN  40529  trnsetN  40532  trlset  40537  trlval  40538  tgrpset  41121  tendoset  41135  tendo02  41163  erngset  41176  erngset-rN  41184  cdlemksv  41220  dvaset  41381  dvaplusgv  41386  diafval  41407  diaval  41408  dvhset  41457  cdlemm10N  41494  docafvalN  41498  djafvalN  41510  dibfval  41517  dibval  41518  dicfval  41551  dicval  41552  dihval  41608  dochfval  41726  djhfval  41773  dochfl1  41852  lpolsetN  41858  lcdval  41965  mapdhval  42100  hvmapfval  42135  hdmap1fval  42172  fimgmcyc  42904  prjspval  42961  isnacs  43061  mzpclval  43082  mzpsubst  43105  mzprename  43106  mzpcompact2lem  43108  eldiophb  43114  diophrw  43116  eldioph2  43119  diophin  43129  diophun  43130  diophren  43170  pell1qrval  43203  pell14qrval  43205  pell1234qrval  43207  pellfundval  43237  rmxypairf1o  43268  rmxyval  43272  mzpcong  43329  pw2f1ocnv  43394  dnnumch1  43401  dfac11  43419  hbtlem1  43480  hbtlem7  43482  elmnc  43493  dgraaval  43501  mpaaval  43508  itgoval  43518  flcidc  43527  mendval  43536  cytpval  43559  cantnfub  43678  cantnfresb  43681  tfsconcatrev  43705  elcnvlem  43957  comptiunov2i  44062  dftrcl3  44076  trclfvcom  44079  cnvtrclfv  44080  cotrcltrcl  44081  trclimalb2  44082  trclfvdecomr  44084  dfrtrcl3  44089  dfrtrcl4  44094  clsk1indlem0  44397  clsk1indlem2  44398  clsk1indlem3  44399  clsk1indlem4  44400  clsk1indlem1  44401  k0004val  44506  lhe4.4ex1a  44685  addrfv  44824  subrfv  44825  mulvfv  44826  monoord2xrv  45841  sumnnodd  45990  liminfgval  46120  ioodvbdlimc2lem  46292  itgsin0pilem1  46308  stoweidlem55  46413  wallispilem1  46423  wallispilem2  46424  wallispilem4  46426  wallispi2lem1  46429  wallispi2lem2  46430  dirkerval  46449  fourierdlem2  46467  fourierdlem3  46468  fourierdlem29  46494  fourierdlem62  46526  fourierdlem80  46544  fourierdlem103  46567  fourierdlem104  46568  fourierswlem  46588  fouriersw  46589  iundjiunlem  46817  carageniuncllem2  46880  0ome  46887  hoidmv1le  46952  hoidmvlelem3  46955  smflimsuplem7  47184  nthrucw  47244  iccpval  47775  fppr  48086  bigoval  48909  ackval0  49040  ackval41a  49054  eenglngeehlnm  49099  oppcinito  49594  oppctermo  49595  dfinito4  49860  prstcval  49910  mndtcval  49938  setc1onsubc  49961  lmdfval2  50014  cmdfval2  50015  vsetrec  50062  onsetreclem1  50064  elpglem3  50072  pgindnf  50075  sinhval-named  50095  coshval-named  50096  tanhval-named  50097  secval  50106  cscval  50107  cotval  50108  aacllem  50160