Theorem fvmpt 6971

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ↦ cmpt 5191  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fvmptex  6985  fvmptrabfv  7003  mptfvmpt  7205  fvmptopab  7446  ofval  7667  caofinvl  7688  fvresex  7941  1stval  7973  2ndval  7974  reldm  8026  curry1val  8087  curry2val  8091  fsplitfpar  8100  fnwelem  8113  brtpos2  8214  onovuni  8314  tz7.44-1  8377  oasuc  8491  oesuclem  8492  omsuc  8493  onasuc  8495  onmsuc  8496  fsetfocdm  8837  fvmptmap  8857  xpcomco  9036  unxpdomlem1  9204  unfilem2  9262  ordtypelem3  9480  ixpiunwdom  9550  inf3lema  9584  noinfep  9620  cantnfval  9628  cantnflem1d  9648  cantnflem1  9649  ssttrcl  9675  ttrcltr  9676  ttrclselem2  9686  r1sucg  9729  r0weon  9972  infxpenc2lem1  9979  fseqenlem1  9984  fseqenlem2  9985  dfac8alem  9989  ac5num  9996  acni2  10006  dfac4  10082  dfac2a  10090  dfacacn  10102  dfac12lem1  10104  ackbij1lem7  10185  ackbij2lem2  10199  ackbij2lem3  10200  cfsmolem  10230  fin23lem28  10300  fin23lem39  10310  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  fin1a2lem3  10362  itunifval  10376  itunisuc  10379  axdc2lem  10408  axdc3lem2  10411  axcclem  10417  zorn2lem1  10456  negiso  12170  infrenegsup  12173  uzval  12802  flval  13763  ceilval  13807  ceilval2  13809  monoord2  14005  seqf1olem2  14014  seqf1o  14015  seqdistr  14025  serle  14029  seqof  14031  swrdfv  14620  revval  14732  revfv  14735  wwlktovf1  14930  wwlktovfo  14931  sgnval  15061  cjval  15075  reval  15079  imval  15080  sqrtval  15210  absval  15211  limsupval  15447  limsupgval  15449  climmpt  15544  climle  15613  rlimdiv  15619  isercolllem1  15638  isercoll2  15642  caurcvg2  15651  fsumser  15703  isumadd  15740  fsumcnv  15746  fsumrev  15752  fsumshft  15753  iserabs  15788  cvgcmp  15789  cvgcmpce  15791  incexclem  15809  isumless  15818  divcnvshft  15828  supcvg  15829  harmonic  15832  trireciplem  15835  trirecip  15836  expcnv  15837  explecnv  15838  geolim  15843  geolim2  15844  geo2lim  15848  geomulcvg  15849  geoisum  15850  geoisumr  15851  geoisum1  15852  geoisum1c  15853  cvgrat  15856  mertenslem2  15858  mertens  15859  prodfdiv  15869  fprodser  15922  fprodshft  15949  fprodrev  15950  fprodcnv  15956  iprodmul  15976  bpolylem  16021  eftval  16049  efval  16052  efcvgfsum  16059  ege2le3  16063  eftlub  16084  eflegeo  16096  sinval  16097  cosval  16098  tanval  16103  eirrlem  16179  rpnnen2lem1  16189  rpnnen2lem2  16190  bitsfval  16400  bitsinv2  16420  bitsinv  16425  sadcf  16430  sadc0  16431  sadcp1  16432  smupf  16455  smup0  16456  smupp1  16457  qnumval  16714  qdenval  16715  phival  16744  crth  16755  phimullem  16756  eulerthlem2  16759  phisum  16768  odzval  16769  iserodd  16813  pcmpt  16870  prmreclem1  16894  prmreclem2  16895  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  1arithlem1  16901  1arithlem2  16902  vdwapfval  16949  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  ramub1lem2  17005  ramcl  17007  prmoval  17011  strfvnd  17162  topnval  17404  prdsplusgfval  17444  prdsmulrfval  17446  isacs  17619  acsfn  17627  homffval  17658  comfffval  17666  oppcval  17681  monfval  17701  oppcmon  17707  sectffval  17719  invffval  17727  isoval  17734  idfuval  17845  homafval  17998  arwval  18012  coafval  18033  yonedainv  18249  oduval  18256  pltfval  18297  lubfval  18316  lubval  18322  glbfval  18329  glbval  18335  p0val  18393  p1val  18394  ipoval  18496  plusffval  18580  grpidval  18595  issubmgm  18636  issubm  18737  prdspjmhm  18763  efmnd  18804  smndex1igid  18838  grpinvfval  18917  grpinvval  18919  grpsubfval  18922  grpsubfvalALT  18923  grplactval  18981  prdsinvlem  18988  mulgfval  19008  mulgfvalALT  19009  pwsmulg  19058  issubg  19065  isnsg  19094  cycsubmel  19139  cycsubgcl  19145  conjghm  19188  conjnmz  19191  cntrval  19258  cntzfval  19259  cntzval  19260  oppgval  19286  psgnfval  19437  psgnval  19444  odfval  19469  odval  19471  sylow1lem4  19538  pgpssslw  19551  sylow2blem3  19559  sylow3lem2  19565  lsmfval  19575  pj1fval  19631  efgval  19654  efgsval  19668  frgpval  19695  vrgpval  19704  mulgmhm  19764  mulgghm  19765  ablfaclem1  20024  mgpval  20059  srglmhm  20137  srgrmhm  20138  ringlghm  20228  ringrghm  20229  pwspjmhmmgpd  20244  pwsexpg  20245  opprval  20254  dvdsrval  20277  isunit  20289  invrfval  20305  dvrfval  20318  isirred  20335  issubrng  20463  issubrg  20487  rgspnval  20528  rrgval  20613  fidomndrnglem  20688  issdrg  20704  abvfval  20726  abvtrivd  20748  staffval  20757  stafval  20758  scaffval  20793  lmodvsghm  20836  lssset  20846  lspfval  20886  islbs  20990  sraval  21089  rlmval  21105  2idlval  21168  lpival  21241  expmhm  21360  expghm  21392  mulgghm2  21393  mulgrhm  21394  zrhval  21424  zrhmulg  21426  zlmval  21432  chrval  21440  znval  21452  znzrhval  21463  evpmss  21502  psgnevpmb  21503  ip0l  21552  ipffval  21564  ocvfval  21582  ocvval  21583  cssval  21598  thlval  21611  pjfval  21622  pjval  21626  isobs  21636  prdsinvgd2  21658  uvcresum  21709  frlmup1  21714  frlmup2  21715  islinds  21725  islindf5  21755  aspval  21789  asclval  21796  psrmulval  21860  psrlidm  21878  psrridm  21879  psrascl  21895  mvrval  21898  mvrval2  21899  mplmonmul  21950  evlslem3  21994  evlslem1  21996  evlsval  22000  evlssca  22003  evlsvar  22004  psdmul  22060  psdmvr  22063  psr1val  22077  vr1val  22083  ply1val  22085  coe1fval  22097  coe1fv  22098  coe1tmmul2  22169  coe1tmmul  22170  coe1tmmul2fv  22171  coe1pwmulfv  22173  evls1val  22214  evl1fval  22222  evl1val  22223  mamulid  22335  mamurid  22336  mdetleib  22481  mdetleib1  22485  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  cpmidpmatlem1  22764  ordtval  23083  cnpval  23130  ptpjpre1  23465  ptpjopn  23506  dfac14  23512  upxp  23517  uptx  23519  hauseqlcld  23540  txlm  23542  xkoptsub  23548  xkoinjcn  23581  kqval  23620  xpstopnlem1  23703  fmval  23837  flfval  23884  ptcmplem2  23947  ptcmplem3  23948  symgtgp  24000  qustgpopn  24014  ussval  24154  iscfilu  24182  ispsmet  24199  ismet  24218  isxmet  24219  mopnval  24333  prdsxmslem2  24424  nmfval  24483  nmval  24484  nmoval  24610  metdsval  24743  divcnOLD  24764  divcn  24766  mulc1cncf  24805  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  cnheiborlem  24860  evth  24865  evth2  24866  lebnumlem3  24869  isphtpy  24887  isphtpc  24900  pcofval  24917  pcovalg  24919  pco1  24922  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevcl  24932  pcorevlem  24933  pcorev2  24935  pi1xfrcnv  24964  cphnm  25100  tcphval  25125  tcphnmval  25136  cfilfval  25171  iscmet  25191  iscmet3lem3  25197  rrxval  25294  ehlval  25321  ivth2  25363  ovolval  25381  ovollb2lem  25396  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem2  25411  ovolicc1  25424  voliunlem1  25458  voliunlem2  25459  voliunlem3  25460  volsup  25464  ioorval  25482  uniioombllem3  25493  uniioombllem6  25496  volsup2  25513  volcn  25514  volivth  25515  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  vitali  25521  mbfmax  25557  mbfimaopnlem  25563  itg1val  25591  i1f1lem  25597  itg11  25599  itg1addlem4  25607  itg1mulc  25612  i1fres  25613  itg1climres  25622  mbfi1fseqlem2  25624  mbfi1fseqlem3  25625  mbfi1fseqlem6  25628  mbfi1flimlem  25630  mbfi1flim  25631  mbfmullem2  25632  itg2seq  25650  itg2uba  25651  itg2splitlem  25656  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2i1fseqle  25662  itg2i1fseq  25663  itg2i1fseq2  25664  itg2addlem  25666  itg2cnlem1  25669  itg2cn  25671  limccnp2  25800  dvnff  25832  dvnp1  25834  cpnfval  25841  elcpn  25843  dvrec  25866  dvcnvlem  25887  dveflem  25890  dvef  25891  dvferm1  25896  dvferm2  25898  rolle  25901  dvlip  25905  dvlipcn  25906  dv11cn  25913  dvivthlem1  25920  dvivth  25922  lhop1lem  25925  ftc1lem1  25949  ftc1lem5  25954  ftc2  25958  itgsubstlem  25962  tdeglem3  25971  tdeglem4  25972  mdegval  25975  mdegmullem  25990  deg1fval  25992  deg1ldg  26004  deg1leb  26007  coe1mul3  26011  uc1pval  26052  mon1pval  26054  mon1pid  26066  q1pval  26067  r1pval  26070  ply1remlem  26077  ig1pval  26088  plyval  26105  elply2  26108  plyeq0lem  26122  coeval  26135  dgrval  26140  coeid2  26151  coemullem  26162  coemul  26164  elqaalem1  26234  elqaalem2  26235  elqaalem3  26236  iaa  26240  aareccl  26241  aannenlem1  26243  geolim3  26254  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem5  26262  aaliou3lem6  26263  aaliou3lem7  26264  aaliou3  26266  tayl0  26276  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmshftlem  26305  ulmshft  26306  ulmuni  26308  ulmcau  26311  ulmdvlem1  26316  ulmdvlem3  26318  mtest  26320  mtestbdd  26321  mbfulm  26322  iblulm  26323  itgulm  26324  pserval  26326  pserval2  26327  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  pserulm  26338  pserdvlem2  26345  pserdv  26346  abelthlem1  26348  abelthlem3  26350  abelthlem4  26351  abelthlem5  26352  abelthlem6  26353  abelthlem7  26355  abelthlem8  26356  abelthlem9  26357  resinf1o  26452  efif1olem4  26461  eff1olem  26464  logcnlem5  26562  logtayllem  26575  logtayl  26576  logtaylsum  26577  logtayl2  26578  logccv  26579  asinval  26799  acosval  26800  atanval  26801  atantayl  26854  leibpilem2  26858  leibpi  26859  leibpisum  26860  log2cnv  26861  log2tlbnd  26862  areaval  26881  efrlim  26886  efrlimOLD  26887  dfef2  26888  amgmlem  26907  emcllem2  26914  emcllem3  26915  emcllem4  26916  emcllem5  26917  emcllem6  26918  emcllem7  26919  zetacvg  26932  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulm2  26953  lgamcvglem  26957  igamval  26964  lgamcvg2  26972  gamcvg2lem  26976  ftalem7  26996  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  basellem6  27003  basellem8  27005  basellem9  27006  chtval  27027  vmaval  27030  chpval  27039  ppival  27044  muval  27049  prmorcht  27095  sqff1o  27099  dvdsflsumcom  27105  musum  27108  muinv  27110  sgmppw  27115  fsumvma  27131  pclogsum  27133  dchrfi  27173  bposlem5  27206  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgsfval  27220  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  lgsqrlem2  27265  lgsqrlem4  27267  lgseisenlem2  27294  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasumiflem1  27419  dchrvmaeq0  27422  dchrisum0fval  27423  dchrisum0re  27431  mulog2sumlem1  27452  pntrval  27480  pntsval  27490  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntlem3  27527  abvcxp  27533  padicfval  27534  padicval  27535  padicabv  27548  ostth1  27551  ostth2  27555  ostth3  27556  nosupfv  27625  noinffv  27640  newval  27770  leftval  27778  rightval  27779  iscgrg  28446  legval  28518  ishpg  28693  iscgra  28743  isinag  28772  isleag  28781  iseqlg  28801  ttgval  28809  elee  28828  axsegconlem1  28851  axsegconlem9  28859  axsegconlem10  28860  axpasch  28875  axlowdimlem15  28890  axlowdim  28895  axeuclidlem  28896  axcontlem2  28899  eengv  28913  vtxval  28934  iedgval  28935  edgval  28983  vtxdgval  29403  wwlksnextinj  29836  wwlksnextsurj  29837  clwwlkfv  29984  clwwlknonmpo  30025  fusgreg2wsplem  30269  fusgreghash2wsp  30274  numclwwlk1lem2fv  30292  gidval  30448  grpoinvval  30459  bafval  30540  imsval  30621  dipfval  30638  sspval  30659  nmooval  30699  hmoval  30746  ipasslem8  30773  ipasslem9  30774  ipblnfi  30791  ubthlem2  30807  htthlem  30853  normval  31060  ocval  31216  occllem  31239  hsupval  31270  pjhfval  31332  pjhval  31333  chscllem2  31574  chscllem3  31575  hosval  31676  homval  31677  hodval  31678  hfsval  31679  hfmval  31680  brafval  31879  braval  31880  kbval  31890  eigvalval  31896  cnlnadjlem1  32003  nmopadjlei  32024  hmopidmchi  32087  strlem2  32187  hstrlem2  32195  cdj3lem2  32371  ofpreima  32596  psgnfzto1stlem  33064  evpmval  33109  altgnsg  33113  inftmrel  33141  isinftm  33142  qusker  33327  qusvscpbl  33329  qusvsval  33330  mxidlval  33439  idlsrgval  33481  dimval  33603  dimvalfi  33604  smatfval  33792  lmatval  33810  locfinreflem  33837  rspecval  33861  rmulccn  33925  xrmulc1cn  33927  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  xrge0iif1  33935  qqhval  33969  rrhval  33993  xrhval  34015  ddeval1  34231  ddeval0  34232  sxbrsigalem0  34269  sxbrsigalem3  34270  eulerpartlemgv  34371  rrvmbfm  34440  dstrvval  34469  coinflippv  34482  ballotlem2  34487  ballotlemfval  34488  ballotlemi  34499  ballotlemsval  34507  ballotlemrval  34516  ballotth  34536  plymulx  34546  signstfv  34561  signsvvfval  34576  onvf1odlem3  35099  derangval  35161  subfacval  35167  erdszelem3  35187  erdszelem9  35193  erdszelem10  35194  txpconn  35226  indispconn  35228  cvxpconn  35236  cvmlift2lem2  35298  cvmlift2lem3  35299  cvmlift2lem7  35303  cvmliftphtlem  35311  cvmlift3lem4  35316  snmlfval  35324  snmlval  35325  gonafv  35344  mvtval  35494  mrsubffval  35501  mrsubcv  35504  mrsubrn  35507  elmrsubrn  35514  msubffval  35517  mvhval  35528  mpstval  35529  mstaval  35538  mclsval  35557  mppsval  35566  sinccvglem  35666  circum  35668  divcnvlin  35727  iprodefisum  35735  iprodgam  35736  faclimlem1  35737  faclimlem2  35738  faclim  35740  iprodfac  35741  faclim2  35742  dfrdg2  35790  findabrcl  36449  dnival  36466  bj-evalval  37070  bj-inftyexpitaudisj  37200  bj-inftyexpiinv  37203  bj-inftyexpidisj  37205  curfv  37601  finixpnum  37606  poimirlem16  37637  poimir  37654  broucube  37655  mblfinlem2  37659  voliunnfl  37665  volsupnfl  37666  itg2addnclem  37672  itg2addnclem3  37674  ftc1cnnc  37693  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702  ftc2nc  37703  fvopabf4g  37723  sdclem2  37743  fdc  37746  lmclim2  37759  geomcau  37760  istotbnd  37770  isbnd  37781  prdsbnd2  37796  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  rrnval  37828  rrncmslem  37833  idlval  38014  pridlval  38034  maxidlval  38040  lshpset  38978  lsatset  38990  lcvfbr  39020  lflset  39059  lflnegcl  39075  lshpkrlem1  39110  lshpkrlem2  39111  lshpkrlem3  39112  ldualset  39125  cmtfvalN  39210  cvrfval  39268  pats  39285  llnset  39506  lplnset  39530  lvolset  39573  lineset  39739  pointsetN  39742  psubspset  39745  pmapval  39758  paddfval  39798  pclfvalN  39890  polfvalN  39905  polvalN  39906  psubclsetN  39937  watvalN  39994  lhpset  39996  lautset  40083  pautsetN  40099  ldilset  40110  ltrnset  40119  dilsetN  40154  trnsetN  40157  trlset  40162  trlval  40163  tgrpset  40746  tendoset  40760  tendo02  40788  erngset  40801  erngset-rN  40809  cdlemksv  40845  dvaset  41006  dvaplusgv  41011  diafval  41032  diaval  41033  dvhset  41082  cdlemm10N  41119  docafvalN  41123  djafvalN  41135  dibfval  41142  dibval  41143  dicfval  41176  dicval  41177  dihval  41233  dochfval  41351  djhfval  41398  dochfl1  41477  lpolsetN  41483  lcdval  41590  mapdhval  41725  hvmapfval  41760  hdmap1fval  41797  fimgmcyc  42529  prjspval  42598  isnacs  42699  mzpclval  42720  mzpsubst  42743  mzprename  42744  mzpcompact2lem  42746  eldiophb  42752  diophrw  42754  eldioph2  42757  diophin  42767  diophun  42768  diophren  42808  pell1qrval  42841  pell14qrval  42843  pell1234qrval  42845  pellfundval  42875  rmxypairf1o  42907  rmxyval  42911  mzpcong  42968  pw2f1ocnv  43033  dnnumch1  43040  dfac11  43058  hbtlem1  43119  hbtlem7  43121  elmnc  43132  dgraaval  43140  mpaaval  43147  itgoval  43157  flcidc  43166  mendval  43175  cytpval  43198  cantnfub  43317  cantnfresb  43320  tfsconcatrev  43344  elcnvlem  43597  comptiunov2i  43702  dftrcl3  43716  trclfvcom  43719  cnvtrclfv  43720  cotrcltrcl  43721  trclimalb2  43722  trclfvdecomr  43724  dfrtrcl3  43729  dfrtrcl4  43734  clsk1indlem0  44037  clsk1indlem2  44038  clsk1indlem3  44039  clsk1indlem4  44040  clsk1indlem1  44041  k0004val  44146  lhe4.4ex1a  44325  addrfv  44465  subrfv  44466  mulvfv  44467  monoord2xrv  45486  sumnnodd  45635  liminfgval  45767  ioodvbdlimc2lem  45939  itgsin0pilem1  45955  stoweidlem55  46060  wallispilem1  46070  wallispilem2  46071  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  dirkerval  46096  fourierdlem2  46114  fourierdlem3  46115  fourierdlem29  46141  fourierdlem62  46173  fourierdlem80  46191  fourierdlem103  46214  fourierdlem104  46215  fourierswlem  46235  fouriersw  46236  iundjiunlem  46464  carageniuncllem2  46527  0ome  46534  hoidmv1le  46599  hoidmvlelem3  46602  smflimsuplem7  46831  iccpval  47420  fppr  47731  bigoval  48542  ackval0  48673  ackval41a  48687  eenglngeehlnm  48732  oppcinito  49228  oppctermo  49229  dfinito4  49494  prstcval  49544  mndtcval  49572  setc1onsubc  49595  lmdfval2  49648  cmdfval2  49649  vsetrec  49696  onsetreclem1  49698  elpglem3  49706  pgindnf  49709  sinhval-named  49729  coshval-named  49730  tanhval-named  49731  secval  49740  cscval  49741  cotval  49742  aacllem  49794