Theorem fvmpt 6941

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptex  6955  fvmptrabfv  6973  mptfvmpt  7174  fvmptopab  7413  ofval  7633  caofinvl  7654  fvresex  7904  1stval  7935  2ndval  7936  reldm  7988  curry1val  8047  curry2val  8051  fsplitfpar  8060  fnwelem  8073  brtpos2  8174  onovuni  8274  tz7.44-1  8337  oasuc  8451  oesuclem  8452  omsuc  8453  onasuc  8455  onmsuc  8456  fsetfocdm  8798  fvmptmap  8819  xpcomco  8995  unxpdomlem1  9156  unfilem2  9206  ordtypelem3  9425  ixpiunwdom  9495  inf3lema  9533  noinfep  9569  cantnfval  9577  cantnflem1d  9597  cantnflem1  9598  ssttrcl  9624  ttrcltr  9625  ttrclselem2  9635  r1sucg  9681  r0weon  9922  infxpenc2lem1  9929  fseqenlem1  9934  fseqenlem2  9935  dfac8alem  9939  ac5num  9946  acni2  9956  dfac4  10032  dfac2a  10040  dfacacn  10052  dfac12lem1  10054  ackbij1lem7  10135  ackbij2lem2  10149  ackbij2lem3  10150  cfsmolem  10180  fin23lem28  10250  fin23lem39  10260  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  fin1a2lem3  10312  itunifval  10326  itunisuc  10329  axdc2lem  10358  axdc3lem2  10361  axcclem  10367  zorn2lem1  10406  negiso  12122  infrenegsup  12125  uzval  12753  flval  13714  ceilval  13758  ceilval2  13760  monoord2  13956  seqf1olem2  13965  seqf1o  13966  seqdistr  13976  serle  13980  seqof  13982  swrdfv  14572  revval  14683  revfv  14686  wwlktovf1  14880  wwlktovfo  14881  sgnval  15011  cjval  15025  reval  15029  imval  15030  sqrtval  15160  absval  15161  limsupval  15397  limsupgval  15399  climmpt  15494  climle  15563  rlimdiv  15569  isercolllem1  15588  isercoll2  15592  caurcvg2  15601  fsumser  15653  isumadd  15690  fsumcnv  15696  fsumrev  15702  fsumshft  15703  iserabs  15738  cvgcmp  15739  cvgcmpce  15741  incexclem  15759  isumless  15768  divcnvshft  15778  supcvg  15779  harmonic  15782  trireciplem  15785  trirecip  15786  expcnv  15787  explecnv  15788  geolim  15793  geolim2  15794  geo2lim  15798  geomulcvg  15799  geoisum  15800  geoisumr  15801  geoisum1  15802  geoisum1c  15803  cvgrat  15806  mertenslem2  15808  mertens  15809  prodfdiv  15819  fprodser  15872  fprodshft  15899  fprodrev  15900  fprodcnv  15906  iprodmul  15926  bpolylem  15971  eftval  15999  efval  16002  efcvgfsum  16009  ege2le3  16013  eftlub  16034  eflegeo  16046  sinval  16047  cosval  16048  tanval  16053  eirrlem  16129  rpnnen2lem1  16139  rpnnen2lem2  16140  bitsfval  16350  bitsinv2  16370  bitsinv  16375  sadcf  16380  sadc0  16381  sadcp1  16382  smupf  16405  smup0  16406  smupp1  16407  qnumval  16664  qdenval  16665  phival  16694  crth  16705  phimullem  16706  eulerthlem2  16709  phisum  16718  odzval  16719  iserodd  16763  pcmpt  16820  prmreclem1  16844  prmreclem2  16845  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  1arithlem1  16851  1arithlem2  16852  vdwapfval  16899  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  ramub1lem2  16955  ramcl  16957  prmoval  16961  strfvnd  17112  topnval  17354  prdsplusgfval  17394  prdsmulrfval  17396  isacs  17574  acsfn  17582  homffval  17613  comfffval  17621  oppcval  17636  monfval  17656  oppcmon  17662  sectffval  17674  invffval  17682  isoval  17689  idfuval  17800  homafval  17953  arwval  17967  coafval  17988  yonedainv  18204  oduval  18211  pltfval  18252  lubfval  18271  lubval  18277  glbfval  18284  glbval  18290  p0val  18348  p1val  18349  ipoval  18453  plusffval  18571  grpidval  18586  issubmgm  18627  issubm  18728  prdspjmhm  18754  efmnd  18795  smndex1igid  18829  grpinvfval  18908  grpinvval  18910  grpsubfval  18913  grpsubfvalALT  18914  grplactval  18972  prdsinvlem  18979  mulgfval  18999  mulgfvalALT  19000  pwsmulg  19049  issubg  19056  isnsg  19084  cycsubmel  19129  cycsubgcl  19135  conjghm  19178  conjnmz  19181  cntrval  19248  cntzfval  19249  cntzval  19250  oppgval  19276  psgnfval  19429  psgnval  19436  odfval  19461  odval  19463  sylow1lem4  19530  pgpssslw  19543  sylow2blem3  19551  sylow3lem2  19557  lsmfval  19567  pj1fval  19623  efgval  19646  efgsval  19660  frgpval  19687  vrgpval  19696  mulgmhm  19756  mulgghm  19757  ablfaclem1  20016  mgpval  20078  srglmhm  20156  srgrmhm  20157  ringlghm  20247  ringrghm  20248  pwspjmhmmgpd  20263  pwsexpg  20264  opprval  20274  dvdsrval  20297  isunit  20309  invrfval  20325  dvrfval  20338  isirred  20355  issubrng  20480  issubrg  20504  rgspnval  20545  rrgval  20630  fidomndrnglem  20705  issdrg  20721  abvfval  20743  abvtrivd  20765  staffval  20774  stafval  20775  scaffval  20831  lmodvsghm  20874  lssset  20884  lspfval  20924  islbs  21028  sraval  21127  rlmval  21143  2idlval  21206  lpival  21279  expmhm  21391  expghm  21430  mulgghm2  21431  mulgrhm  21432  zrhval  21462  zrhmulg  21464  zlmval  21470  chrval  21478  znval  21490  znzrhval  21501  evpmss  21541  psgnevpmb  21542  ip0l  21591  ipffval  21603  ocvfval  21621  ocvval  21622  cssval  21637  thlval  21650  pjfval  21661  pjval  21665  isobs  21675  prdsinvgd2  21697  uvcresum  21748  frlmup1  21753  frlmup2  21754  islinds  21764  islindf5  21794  aspval  21828  asclval  21835  psrmulval  21900  psrlidm  21917  psrridm  21918  psrascl  21934  mvrval  21937  mvrval2  21938  mplmonmul  21991  evlslem3  22035  evlslem1  22037  evlsval  22041  evlssca  22049  evlsvar  22050  psdmul  22109  psdmvr  22112  psr1val  22126  vr1val  22132  ply1val  22134  coe1fval  22146  coe1fv  22147  coe1tmmul2  22218  coe1tmmul  22219  coe1tmmul2fv  22220  coe1pwmulfv  22222  evls1val  22264  evl1fval  22272  evl1val  22273  mamulid  22385  mamurid  22386  mdetleib  22531  mdetleib1  22535  mdetunilem9  22564  mdetuni0  22565  mdetmul  22567  cpmidpmatlem1  22814  ordtval  23133  cnpval  23180  ptpjpre1  23515  ptpjopn  23556  dfac14  23562  upxp  23567  uptx  23569  hauseqlcld  23590  txlm  23592  xkoptsub  23598  xkoinjcn  23631  kqval  23670  xpstopnlem1  23753  fmval  23887  flfval  23934  ptcmplem2  23997  ptcmplem3  23998  symgtgp  24050  qustgpopn  24064  ussval  24203  iscfilu  24231  ispsmet  24248  ismet  24267  isxmet  24268  mopnval  24382  prdsxmslem2  24473  nmfval  24532  nmval  24533  nmoval  24659  metdsval  24792  divcnOLD  24813  divcn  24815  mulc1cncf  24854  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  cnheiborlem  24909  evth  24914  evth2  24915  lebnumlem3  24918  isphtpy  24936  isphtpc  24949  pcofval  24966  pcovalg  24968  pco1  24971  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevcl  24981  pcorevlem  24982  pcorev2  24984  pi1xfrcnv  25013  cphnm  25149  tcphval  25174  tcphnmval  25185  cfilfval  25220  iscmet  25240  iscmet3lem3  25246  rrxval  25343  ehlval  25370  ivth2  25412  ovolval  25430  ovollb2lem  25445  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem2  25460  ovolicc1  25473  voliunlem1  25507  voliunlem2  25508  voliunlem3  25509  volsup  25513  ioorval  25531  uniioombllem3  25542  uniioombllem6  25545  volsup2  25562  volcn  25563  volivth  25564  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  vitali  25570  mbfmax  25606  mbfimaopnlem  25612  itg1val  25640  i1f1lem  25646  itg11  25648  itg1addlem4  25656  itg1mulc  25661  i1fres  25662  itg1climres  25671  mbfi1fseqlem2  25673  mbfi1fseqlem3  25674  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfi1flim  25680  mbfmullem2  25681  itg2seq  25699  itg2uba  25700  itg2splitlem  25705  itg2monolem1  25707  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  itg2cnlem1  25718  itg2cn  25720  limccnp2  25849  dvnff  25881  dvnp1  25883  cpnfval  25890  elcpn  25892  dvrec  25915  dvcnvlem  25936  dveflem  25939  dvef  25940  dvferm1  25945  dvferm2  25947  rolle  25950  dvlip  25954  dvlipcn  25955  dv11cn  25962  dvivthlem1  25969  dvivth  25971  lhop1lem  25974  ftc1lem1  25998  ftc1lem5  26003  ftc2  26007  itgsubstlem  26011  tdeglem3  26020  tdeglem4  26021  mdegval  26024  mdegmullem  26039  deg1fval  26041  deg1ldg  26053  deg1leb  26056  coe1mul3  26060  uc1pval  26101  mon1pval  26103  mon1pid  26115  q1pval  26116  r1pval  26119  ply1remlem  26126  ig1pval  26137  plyval  26154  elply2  26157  plyeq0lem  26171  coeval  26184  dgrval  26189  coeid2  26200  coemullem  26211  coemul  26213  elqaalem1  26283  elqaalem2  26284  elqaalem3  26285  iaa  26289  aareccl  26290  aannenlem1  26292  geolim3  26303  aaliou3lem1  26306  aaliou3lem2  26307  aaliou3lem5  26311  aaliou3lem6  26312  aaliou3lem7  26313  aaliou3  26315  tayl0  26325  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  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  26394  pserdv  26395  abelthlem1  26397  abelthlem3  26399  abelthlem4  26400  abelthlem5  26401  abelthlem6  26402  abelthlem7  26404  abelthlem8  26405  abelthlem9  26406  resinf1o  26501  efif1olem4  26510  eff1olem  26513  logcnlem5  26611  logtayllem  26624  logtayl  26625  logtaylsum  26626  logtayl2  26627  logccv  26628  asinval  26848  acosval  26849  atanval  26850  atantayl  26903  leibpilem2  26907  leibpi  26908  leibpisum  26909  log2cnv  26910  log2tlbnd  26911  areaval  26930  efrlim  26935  efrlimOLD  26936  dfef2  26937  amgmlem  26956  emcllem2  26963  emcllem3  26964  emcllem4  26965  emcllem5  26966  emcllem6  26967  emcllem7  26968  zetacvg  26981  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulm2  27002  lgamcvglem  27006  igamval  27013  lgamcvg2  27021  gamcvg2lem  27025  ftalem7  27045  basellem2  27048  basellem3  27049  basellem4  27050  basellem5  27051  basellem6  27052  basellem8  27054  basellem9  27055  chtval  27076  vmaval  27079  chpval  27088  ppival  27093  muval  27098  prmorcht  27144  sqff1o  27148  dvdsflsumcom  27154  musum  27157  muinv  27159  sgmppw  27164  fsumvma  27180  pclogsum  27182  dchrfi  27222  bposlem5  27255  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgsfval  27269  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  lgsqrlem2  27314  lgsqrlem4  27316  lgseisenlem2  27343  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasumiflem1  27468  dchrvmaeq0  27471  dchrisum0fval  27472  dchrisum0re  27480  mulog2sumlem1  27501  pntrval  27529  pntsval  27539  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntlem3  27576  abvcxp  27582  padicfval  27583  padicval  27584  padicabv  27597  ostth1  27600  ostth2  27604  ostth3  27605  nosupfv  27674  noinffv  27689  newval  27831  leftval  27845  rightval  27846  iscgrg  28584  legval  28656  ishpg  28831  iscgra  28881  isinag  28910  isleag  28919  iseqlg  28939  ttgval  28947  elee  28966  axsegconlem1  28990  axsegconlem9  28998  axsegconlem10  28999  axpasch  29014  axlowdimlem15  29029  axlowdim  29034  axeuclidlem  29035  axcontlem2  29038  eengv  29052  vtxval  29073  iedgval  29074  edgval  29122  vtxdgval  29542  wwlksnextinj  29972  wwlksnextsurj  29973  clwwlkfv  30123  clwwlknonmpo  30164  fusgreg2wsplem  30408  fusgreghash2wsp  30413  numclwwlk1lem2fv  30431  gidval  30587  grpoinvval  30598  bafval  30679  imsval  30760  dipfval  30777  sspval  30798  nmooval  30838  hmoval  30885  ipasslem8  30912  ipasslem9  30913  ipblnfi  30930  ubthlem2  30946  htthlem  30992  normval  31199  ocval  31355  occllem  31378  hsupval  31409  pjhfval  31471  pjhval  31472  chscllem2  31713  chscllem3  31714  hosval  31815  homval  31816  hodval  31817  hfsval  31818  hfmval  31819  brafval  32018  braval  32019  kbval  32029  eigvalval  32035  cnlnadjlem1  32142  nmopadjlei  32163  hmopidmchi  32226  strlem2  32326  hstrlem2  32334  cdj3lem2  32510  ofpreima  32743  psgnfzto1stlem  33182  evpmval  33227  altgnsg  33231  inftmrel  33262  isinftm  33263  qusker  33430  qusvscpbl  33432  qusvsval  33433  mxidlval  33542  idlsrgval  33584  dimval  33757  dimvalfi  33758  smatfval  33952  lmatval  33970  locfinreflem  33997  rspecval  34021  rmulccn  34085  xrmulc1cn  34087  xrge0iifcv  34091  xrge0iifiso  34092  xrge0iifhom  34094  xrge0iif1  34095  qqhval  34129  rrhval  34153  xrhval  34175  ddeval1  34391  ddeval0  34392  sxbrsigalem0  34428  sxbrsigalem3  34429  eulerpartlemgv  34530  rrvmbfm  34599  dstrvval  34628  coinflippv  34641  ballotlem2  34646  ballotlemfval  34647  ballotlemi  34658  ballotlemsval  34666  ballotlemrval  34675  ballotth  34695  plymulx  34705  signstfv  34720  signsvvfval  34735  onvf1odlem3  35299  derangval  35361  subfacval  35367  erdszelem3  35387  erdszelem9  35393  erdszelem10  35394  txpconn  35426  indispconn  35428  cvxpconn  35436  cvmlift2lem2  35498  cvmlift2lem3  35499  cvmlift2lem7  35503  cvmliftphtlem  35511  cvmlift3lem4  35516  snmlfval  35524  snmlval  35525  gonafv  35544  mvtval  35694  mrsubffval  35701  mrsubcv  35704  mrsubrn  35707  elmrsubrn  35714  msubffval  35717  mvhval  35728  mpstval  35729  mstaval  35738  mclsval  35757  mppsval  35766  sinccvglem  35866  circum  35868  divcnvlin  35927  iprodefisum  35935  iprodgam  35936  faclimlem1  35937  faclimlem2  35938  faclim  35940  iprodfac  35941  faclim2  35942  dfrdg2  35987  findabrcl  36648  dnival  36671  bj-evalval  37280  bj-inftyexpitaudisj  37410  bj-inftyexpiinv  37413  bj-inftyexpidisj  37415  curfv  37801  finixpnum  37806  poimirlem16  37837  poimir  37854  broucube  37855  mblfinlem2  37859  voliunnfl  37865  volsupnfl  37866  itg2addnclem  37872  itg2addnclem3  37874  ftc1cnnc  37893  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anc  37902  ftc2nc  37903  fvopabf4g  37923  sdclem2  37943  fdc  37946  lmclim2  37959  geomcau  37960  istotbnd  37970  isbnd  37981  prdsbnd2  37996  heiborlem6  38017  heiborlem7  38018  heiborlem8  38019  rrnval  38028  rrncmslem  38033  idlval  38214  pridlval  38234  maxidlval  38240  lshpset  39238  lsatset  39250  lcvfbr  39280  lflset  39319  lflnegcl  39335  lshpkrlem1  39370  lshpkrlem2  39371  lshpkrlem3  39372  ldualset  39385  cmtfvalN  39470  cvrfval  39528  pats  39545  llnset  39765  lplnset  39789  lvolset  39832  lineset  39998  pointsetN  40001  psubspset  40004  pmapval  40017  paddfval  40057  pclfvalN  40149  polfvalN  40164  polvalN  40165  psubclsetN  40196  watvalN  40253  lhpset  40255  lautset  40342  pautsetN  40358  ldilset  40369  ltrnset  40378  dilsetN  40413  trnsetN  40416  trlset  40421  trlval  40422  tgrpset  41005  tendoset  41019  tendo02  41047  erngset  41060  erngset-rN  41068  cdlemksv  41104  dvaset  41265  dvaplusgv  41270  diafval  41291  diaval  41292  dvhset  41341  cdlemm10N  41378  docafvalN  41382  djafvalN  41394  dibfval  41401  dibval  41402  dicfval  41435  dicval  41436  dihval  41492  dochfval  41610  djhfval  41657  dochfl1  41736  lpolsetN  41742  lcdval  41849  mapdhval  41984  hvmapfval  42019  hdmap1fval  42056  fimgmcyc  42789  prjspval  42846  isnacs  42946  mzpclval  42967  mzpsubst  42990  mzprename  42991  mzpcompact2lem  42993  eldiophb  42999  diophrw  43001  eldioph2  43004  diophin  43014  diophun  43015  diophren  43055  pell1qrval  43088  pell14qrval  43090  pell1234qrval  43092  pellfundval  43122  rmxypairf1o  43153  rmxyval  43157  mzpcong  43214  pw2f1ocnv  43279  dnnumch1  43286  dfac11  43304  hbtlem1  43365  hbtlem7  43367  elmnc  43378  dgraaval  43386  mpaaval  43393  itgoval  43403  flcidc  43412  mendval  43421  cytpval  43444  cantnfub  43563  cantnfresb  43566  tfsconcatrev  43590  elcnvlem  43842  comptiunov2i  43947  dftrcl3  43961  trclfvcom  43964  cnvtrclfv  43965  cotrcltrcl  43966  trclimalb2  43967  trclfvdecomr  43969  dfrtrcl3  43974  dfrtrcl4  43979  clsk1indlem0  44282  clsk1indlem2  44283  clsk1indlem3  44284  clsk1indlem4  44285  clsk1indlem1  44286  k0004val  44391  lhe4.4ex1a  44570  addrfv  44709  subrfv  44710  mulvfv  44711  monoord2xrv  45727  sumnnodd  45876  liminfgval  46006  ioodvbdlimc2lem  46178  itgsin0pilem1  46194  stoweidlem55  46299  wallispilem1  46309  wallispilem2  46310  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  dirkerval  46335  fourierdlem2  46353  fourierdlem3  46354  fourierdlem29  46380  fourierdlem62  46412  fourierdlem80  46430  fourierdlem103  46453  fourierdlem104  46454  fourierswlem  46474  fouriersw  46475  iundjiunlem  46703  carageniuncllem2  46766  0ome  46773  hoidmv1le  46838  hoidmvlelem3  46841  smflimsuplem7  47070  nthrucw  47130  iccpval  47661  fppr  47972  bigoval  48795  ackval0  48926  ackval41a  48940  eenglngeehlnm  48985  oppcinito  49480  oppctermo  49481  dfinito4  49746  prstcval  49796  mndtcval  49824  setc1onsubc  49847  lmdfval2  49900  cmdfval2  49901  vsetrec  49948  onsetreclem1  49950  elpglem3  49958  pgindnf  49961  sinhval-named  49981  coshval-named  49982  tanhval-named  49983  secval  49992  cscval  49993  cotval  49994  aacllem  50046