Theorem fvmpt 6968

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ↦ cmpt 5188  ‘cfv 6511

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvmptex  6982  fvmptrabfv  7000  mptfvmpt  7202  fvmptopab  7443  ofval  7664  caofinvl  7685  fvresex  7938  1stval  7970  2ndval  7971  reldm  8023  curry1val  8084  curry2val  8088  fsplitfpar  8097  fnwelem  8110  brtpos2  8211  onovuni  8311  tz7.44-1  8374  oasuc  8488  oesuclem  8489  omsuc  8490  onasuc  8492  onmsuc  8493  fsetfocdm  8834  fvmptmap  8854  xpcomco  9031  unxpdomlem1  9197  unfilem2  9255  ordtypelem3  9473  ixpiunwdom  9543  inf3lema  9577  noinfep  9613  cantnfval  9621  cantnflem1d  9641  cantnflem1  9642  ssttrcl  9668  ttrcltr  9669  ttrclselem2  9679  r1sucg  9722  r0weon  9965  infxpenc2lem1  9972  fseqenlem1  9977  fseqenlem2  9978  dfac8alem  9982  ac5num  9989  acni2  9999  dfac4  10075  dfac2a  10083  dfacacn  10095  dfac12lem1  10097  ackbij1lem7  10178  ackbij2lem2  10192  ackbij2lem3  10193  cfsmolem  10223  fin23lem28  10293  fin23lem39  10303  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  fin1a2lem3  10355  itunifval  10369  itunisuc  10372  axdc2lem  10401  axdc3lem2  10404  axcclem  10410  zorn2lem1  10449  negiso  12163  infrenegsup  12166  uzval  12795  flval  13756  ceilval  13800  ceilval2  13802  monoord2  13998  seqf1olem2  14007  seqf1o  14008  seqdistr  14018  serle  14022  seqof  14024  swrdfv  14613  revval  14725  revfv  14728  wwlktovf1  14923  wwlktovfo  14924  sgnval  15054  cjval  15068  reval  15072  imval  15073  sqrtval  15203  absval  15204  limsupval  15440  limsupgval  15442  climmpt  15537  climle  15606  rlimdiv  15612  isercolllem1  15631  isercoll2  15635  caurcvg2  15644  fsumser  15696  isumadd  15733  fsumcnv  15739  fsumrev  15745  fsumshft  15746  iserabs  15781  cvgcmp  15782  cvgcmpce  15784  incexclem  15802  isumless  15811  divcnvshft  15821  supcvg  15822  harmonic  15825  trireciplem  15828  trirecip  15829  expcnv  15830  explecnv  15831  geolim  15836  geolim2  15837  geo2lim  15841  geomulcvg  15842  geoisum  15843  geoisumr  15844  geoisum1  15845  geoisum1c  15846  cvgrat  15849  mertenslem2  15851  mertens  15852  prodfdiv  15862  fprodser  15915  fprodshft  15942  fprodrev  15943  fprodcnv  15949  iprodmul  15969  bpolylem  16014  eftval  16042  efval  16045  efcvgfsum  16052  ege2le3  16056  eftlub  16077  eflegeo  16089  sinval  16090  cosval  16091  tanval  16096  eirrlem  16172  rpnnen2lem1  16182  rpnnen2lem2  16183  bitsfval  16393  bitsinv2  16413  bitsinv  16418  sadcf  16423  sadc0  16424  sadcp1  16425  smupf  16448  smup0  16449  smupp1  16450  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  17612  acsfn  17620  homffval  17651  comfffval  17659  oppcval  17674  monfval  17694  oppcmon  17700  sectffval  17712  invffval  17720  isoval  17727  idfuval  17838  homafval  17991  arwval  18005  coafval  18026  yonedainv  18242  oduval  18249  pltfval  18290  lubfval  18309  lubval  18315  glbfval  18322  glbval  18328  p0val  18386  p1val  18387  ipoval  18489  plusffval  18573  grpidval  18588  issubmgm  18629  issubm  18730  prdspjmhm  18756  efmnd  18797  smndex1igid  18831  grpinvfval  18910  grpinvval  18912  grpsubfval  18915  grpsubfvalALT  18916  grplactval  18974  prdsinvlem  18981  mulgfval  19001  mulgfvalALT  19002  pwsmulg  19051  issubg  19058  isnsg  19087  cycsubmel  19132  cycsubgcl  19138  conjghm  19181  conjnmz  19184  cntrval  19251  cntzfval  19252  cntzval  19253  oppgval  19279  psgnfval  19430  psgnval  19437  odfval  19462  odval  19464  sylow1lem4  19531  pgpssslw  19544  sylow2blem3  19552  sylow3lem2  19558  lsmfval  19568  pj1fval  19624  efgval  19647  efgsval  19661  frgpval  19688  vrgpval  19697  mulgmhm  19757  mulgghm  19758  ablfaclem1  20017  mgpval  20052  srglmhm  20130  srgrmhm  20131  ringlghm  20221  ringrghm  20222  pwspjmhmmgpd  20237  pwsexpg  20238  opprval  20247  dvdsrval  20270  isunit  20282  invrfval  20298  dvrfval  20311  isirred  20328  issubrng  20456  issubrg  20480  rgspnval  20521  rrgval  20606  fidomndrnglem  20681  issdrg  20697  abvfval  20719  abvtrivd  20741  staffval  20750  stafval  20751  scaffval  20786  lmodvsghm  20829  lssset  20839  lspfval  20879  islbs  20983  sraval  21082  rlmval  21098  2idlval  21161  lpival  21234  expmhm  21353  expghm  21385  mulgghm2  21386  mulgrhm  21387  zrhval  21417  zrhmulg  21419  zlmval  21425  chrval  21433  znval  21445  znzrhval  21456  evpmss  21495  psgnevpmb  21496  ip0l  21545  ipffval  21557  ocvfval  21575  ocvval  21576  cssval  21591  thlval  21604  pjfval  21615  pjval  21619  isobs  21629  prdsinvgd2  21651  uvcresum  21702  frlmup1  21707  frlmup2  21708  islinds  21718  islindf5  21748  aspval  21782  asclval  21789  psrmulval  21853  psrlidm  21871  psrridm  21872  psrascl  21888  mvrval  21891  mvrval2  21892  mplmonmul  21943  evlslem3  21987  evlslem1  21989  evlsval  21993  evlssca  21996  evlsvar  21997  psdmul  22053  psdmvr  22056  psr1val  22070  vr1val  22076  ply1val  22078  coe1fval  22090  coe1fv  22091  coe1tmmul2  22162  coe1tmmul  22163  coe1tmmul2fv  22164  coe1pwmulfv  22166  evls1val  22207  evl1fval  22215  evl1val  22216  mamulid  22328  mamurid  22329  mdetleib  22474  mdetleib1  22478  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  cpmidpmatlem1  22757  ordtval  23076  cnpval  23123  ptpjpre1  23458  ptpjopn  23499  dfac14  23505  upxp  23510  uptx  23512  hauseqlcld  23533  txlm  23535  xkoptsub  23541  xkoinjcn  23574  kqval  23613  xpstopnlem1  23696  fmval  23830  flfval  23877  ptcmplem2  23940  ptcmplem3  23941  symgtgp  23993  qustgpopn  24007  ussval  24147  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  mopnval  24326  prdsxmslem2  24417  nmfval  24476  nmval  24477  nmoval  24603  metdsval  24736  divcnOLD  24757  divcn  24759  mulc1cncf  24798  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  cnheiborlem  24853  evth  24858  evth2  24859  lebnumlem3  24862  isphtpy  24880  isphtpc  24893  pcofval  24910  pcovalg  24912  pco1  24915  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevcl  24925  pcorevlem  24926  pcorev2  24928  pi1xfrcnv  24957  cphnm  25093  tcphval  25118  tcphnmval  25129  cfilfval  25164  iscmet  25184  iscmet3lem3  25190  rrxval  25287  ehlval  25314  ivth2  25356  ovolval  25374  ovollb2lem  25389  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovolicc1  25417  voliunlem1  25451  voliunlem2  25452  voliunlem3  25453  volsup  25457  ioorval  25475  uniioombllem3  25486  uniioombllem6  25489  volsup2  25506  volcn  25507  volivth  25508  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  vitali  25514  mbfmax  25550  mbfimaopnlem  25556  itg1val  25584  i1f1lem  25590  itg11  25592  itg1addlem4  25600  itg1mulc  25605  i1fres  25606  itg1climres  25615  mbfi1fseqlem2  25617  mbfi1fseqlem3  25618  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfi1flim  25624  mbfmullem2  25625  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  itg2cnlem1  25662  itg2cn  25664  limccnp2  25793  dvnff  25825  dvnp1  25827  cpnfval  25834  elcpn  25836  dvrec  25859  dvcnvlem  25880  dveflem  25883  dvef  25884  dvferm1  25889  dvferm2  25891  rolle  25894  dvlip  25898  dvlipcn  25899  dv11cn  25906  dvivthlem1  25913  dvivth  25915  lhop1lem  25918  ftc1lem1  25942  ftc1lem5  25947  ftc2  25951  itgsubstlem  25955  tdeglem3  25964  tdeglem4  25965  mdegval  25968  mdegmullem  25983  deg1fval  25985  deg1ldg  25997  deg1leb  26000  coe1mul3  26004  uc1pval  26045  mon1pval  26047  mon1pid  26059  q1pval  26060  r1pval  26063  ply1remlem  26070  ig1pval  26081  plyval  26098  elply2  26101  plyeq0lem  26115  coeval  26128  dgrval  26133  coeid2  26144  coemullem  26155  coemul  26157  elqaalem1  26227  elqaalem2  26228  elqaalem3  26229  iaa  26233  aareccl  26234  aannenlem1  26236  geolim3  26247  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  aaliou3  26259  tayl0  26269  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmshftlem  26298  ulmshft  26299  ulmuni  26301  ulmcau  26304  ulmdvlem1  26309  ulmdvlem3  26311  mtest  26313  mtestbdd  26314  mbfulm  26315  iblulm  26316  itgulm  26317  pserval  26319  pserval2  26320  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  pserulm  26331  pserdvlem2  26338  pserdv  26339  abelthlem1  26341  abelthlem3  26343  abelthlem4  26344  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  abelthlem8  26349  abelthlem9  26350  resinf1o  26445  efif1olem4  26454  eff1olem  26457  logcnlem5  26555  logtayllem  26568  logtayl  26569  logtaylsum  26570  logtayl2  26571  logccv  26572  asinval  26792  acosval  26793  atanval  26794  atantayl  26847  leibpilem2  26851  leibpi  26852  leibpisum  26853  log2cnv  26854  log2tlbnd  26855  areaval  26874  efrlim  26879  efrlimOLD  26880  dfef2  26881  amgmlem  26900  emcllem2  26907  emcllem3  26908  emcllem4  26909  emcllem5  26910  emcllem6  26911  emcllem7  26912  zetacvg  26925  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulm2  26946  lgamcvglem  26950  igamval  26957  lgamcvg2  26965  gamcvg2lem  26969  ftalem7  26989  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  basellem6  26996  basellem8  26998  basellem9  26999  chtval  27020  vmaval  27023  chpval  27032  ppival  27037  muval  27042  prmorcht  27088  sqff1o  27092  dvdsflsumcom  27098  musum  27101  muinv  27103  sgmppw  27108  fsumvma  27124  pclogsum  27126  dchrfi  27166  bposlem5  27199  bposlem7  27201  bposlem8  27202  bposlem9  27203  lgsfval  27213  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgsqrlem2  27258  lgsqrlem4  27260  lgseisenlem2  27287  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasumiflem1  27412  dchrvmaeq0  27415  dchrisum0fval  27416  dchrisum0re  27424  mulog2sumlem1  27445  pntrval  27473  pntsval  27483  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntlem3  27520  abvcxp  27526  padicfval  27527  padicval  27528  padicabv  27541  ostth1  27544  ostth2  27548  ostth3  27549  nosupfv  27618  noinffv  27633  newval  27763  leftval  27771  rightval  27772  iscgrg  28439  legval  28511  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  iseqlg  28794  ttgval  28802  elee  28821  axsegconlem1  28844  axsegconlem9  28852  axsegconlem10  28853  axpasch  28868  axlowdimlem15  28883  axlowdim  28888  axeuclidlem  28889  axcontlem2  28892  eengv  28906  vtxval  28927  iedgval  28928  edgval  28976  vtxdgval  29396  wwlksnextinj  29829  wwlksnextsurj  29830  clwwlkfv  29977  clwwlknonmpo  30018  fusgreg2wsplem  30262  fusgreghash2wsp  30267  numclwwlk1lem2fv  30285  gidval  30441  grpoinvval  30452  bafval  30533  imsval  30614  dipfval  30631  sspval  30652  nmooval  30692  hmoval  30739  ipasslem8  30766  ipasslem9  30767  ipblnfi  30784  ubthlem2  30800  htthlem  30846  normval  31053  ocval  31209  occllem  31232  hsupval  31263  pjhfval  31325  pjhval  31326  chscllem2  31567  chscllem3  31568  hosval  31669  homval  31670  hodval  31671  hfsval  31672  hfmval  31673  brafval  31872  braval  31873  kbval  31883  eigvalval  31889  cnlnadjlem1  31996  nmopadjlei  32017  hmopidmchi  32080  strlem2  32180  hstrlem2  32188  cdj3lem2  32364  ofpreima  32589  psgnfzto1stlem  33057  evpmval  33102  altgnsg  33106  inftmrel  33134  isinftm  33135  qusker  33320  qusvscpbl  33322  qusvsval  33323  mxidlval  33432  idlsrgval  33474  dimval  33596  dimvalfi  33597  smatfval  33785  lmatval  33803  locfinreflem  33830  rspecval  33854  rmulccn  33918  xrmulc1cn  33920  xrge0iifcv  33924  xrge0iifiso  33925  xrge0iifhom  33927  xrge0iif1  33928  qqhval  33962  rrhval  33986  xrhval  34008  ddeval1  34224  ddeval0  34225  sxbrsigalem0  34262  sxbrsigalem3  34263  eulerpartlemgv  34364  rrvmbfm  34433  dstrvval  34462  coinflippv  34475  ballotlem2  34480  ballotlemfval  34481  ballotlemi  34492  ballotlemsval  34500  ballotlemrval  34509  ballotth  34529  plymulx  34539  signstfv  34554  signsvvfval  34569  onvf1odlem3  35092  derangval  35154  subfacval  35160  erdszelem3  35180  erdszelem9  35186  erdszelem10  35187  txpconn  35219  indispconn  35221  cvxpconn  35229  cvmlift2lem2  35291  cvmlift2lem3  35292  cvmlift2lem7  35296  cvmliftphtlem  35304  cvmlift3lem4  35309  snmlfval  35317  snmlval  35318  gonafv  35337  mvtval  35487  mrsubffval  35494  mrsubcv  35497  mrsubrn  35500  elmrsubrn  35507  msubffval  35510  mvhval  35521  mpstval  35522  mstaval  35531  mclsval  35550  mppsval  35559  sinccvglem  35659  circum  35661  divcnvlin  35720  iprodefisum  35728  iprodgam  35729  faclimlem1  35730  faclimlem2  35731  faclim  35733  iprodfac  35734  faclim2  35735  dfrdg2  35783  findabrcl  36442  dnival  36459  bj-evalval  37063  bj-inftyexpitaudisj  37193  bj-inftyexpiinv  37196  bj-inftyexpidisj  37198  curfv  37594  finixpnum  37599  poimirlem16  37630  poimir  37647  broucube  37648  mblfinlem2  37652  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  itg2addnclem3  37667  ftc1cnnc  37686  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  ftc2nc  37696  fvopabf4g  37716  sdclem2  37736  fdc  37739  lmclim2  37752  geomcau  37753  istotbnd  37763  isbnd  37774  prdsbnd2  37789  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  rrnval  37821  rrncmslem  37826  idlval  38007  pridlval  38027  maxidlval  38033  lshpset  38971  lsatset  38983  lcvfbr  39013  lflset  39052  lflnegcl  39068  lshpkrlem1  39103  lshpkrlem2  39104  lshpkrlem3  39105  ldualset  39118  cmtfvalN  39203  cvrfval  39261  pats  39278  llnset  39499  lplnset  39523  lvolset  39566  lineset  39732  pointsetN  39735  psubspset  39738  pmapval  39751  paddfval  39791  pclfvalN  39883  polfvalN  39898  polvalN  39899  psubclsetN  39930  watvalN  39987  lhpset  39989  lautset  40076  pautsetN  40092  ldilset  40103  ltrnset  40112  dilsetN  40147  trnsetN  40150  trlset  40155  trlval  40156  tgrpset  40739  tendoset  40753  tendo02  40781  erngset  40794  erngset-rN  40802  cdlemksv  40838  dvaset  40999  dvaplusgv  41004  diafval  41025  diaval  41026  dvhset  41075  cdlemm10N  41112  docafvalN  41116  djafvalN  41128  dibfval  41135  dibval  41136  dicfval  41169  dicval  41170  dihval  41226  dochfval  41344  djhfval  41391  dochfl1  41470  lpolsetN  41476  lcdval  41583  mapdhval  41718  hvmapfval  41753  hdmap1fval  41790  fimgmcyc  42522  prjspval  42591  isnacs  42692  mzpclval  42713  mzpsubst  42736  mzprename  42737  mzpcompact2lem  42739  eldiophb  42745  diophrw  42747  eldioph2  42750  diophin  42760  diophun  42761  diophren  42801  pell1qrval  42834  pell14qrval  42836  pell1234qrval  42838  pellfundval  42868  rmxypairf1o  42900  rmxyval  42904  mzpcong  42961  pw2f1ocnv  43026  dnnumch1  43033  dfac11  43051  hbtlem1  43112  hbtlem7  43114  elmnc  43125  dgraaval  43133  mpaaval  43140  itgoval  43150  flcidc  43159  mendval  43168  cytpval  43191  cantnfub  43310  cantnfresb  43313  tfsconcatrev  43337  elcnvlem  43590  comptiunov2i  43695  dftrcl3  43709  trclfvcom  43712  cnvtrclfv  43713  cotrcltrcl  43714  trclimalb2  43715  trclfvdecomr  43717  dfrtrcl3  43722  dfrtrcl4  43727  clsk1indlem0  44030  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  k0004val  44139  lhe4.4ex1a  44318  addrfv  44458  subrfv  44459  mulvfv  44460  monoord2xrv  45479  sumnnodd  45628  liminfgval  45760  ioodvbdlimc2lem  45932  itgsin0pilem1  45948  stoweidlem55  46053  wallispilem1  46063  wallispilem2  46064  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  dirkerval  46089  fourierdlem2  46107  fourierdlem3  46108  fourierdlem29  46134  fourierdlem62  46166  fourierdlem80  46184  fourierdlem103  46207  fourierdlem104  46208  fourierswlem  46228  fouriersw  46229  iundjiunlem  46457  carageniuncllem2  46520  0ome  46527  hoidmv1le  46592  hoidmvlelem3  46595  smflimsuplem7  46824  iccpval  47416  fppr  47727  bigoval  48538  ackval0  48669  ackval41a  48683  eenglngeehlnm  48728  oppcinito  49224  oppctermo  49225  dfinito4  49490  prstcval  49540  mndtcval  49568  setc1onsubc  49591  lmdfval2  49644  cmdfval2  49645  vsetrec  49692  onsetreclem1  49694  elpglem3  49702  pgindnf  49705  sinhval-named  49725  coshval-named  49726  tanhval-named  49727  secval  49736  cscval  49737  cotval  49738  aacllem  49790