Theorem fvmpt 6929

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ↦ cmpt 5172  ‘cfv 6481

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  fvmptex  6943  fvmptrabfv  6961  mptfvmpt  7162  fvmptopab  7401  ofval  7621  caofinvl  7642  fvresex  7892  1stval  7923  2ndval  7924  reldm  7976  curry1val  8035  curry2val  8039  fsplitfpar  8048  fnwelem  8061  brtpos2  8162  onovuni  8262  tz7.44-1  8325  oasuc  8439  oesuclem  8440  omsuc  8441  onasuc  8443  onmsuc  8444  fsetfocdm  8785  fvmptmap  8805  xpcomco  8980  unxpdomlem1  9140  unfilem2  9190  ordtypelem3  9406  ixpiunwdom  9476  inf3lema  9514  noinfep  9550  cantnfval  9558  cantnflem1d  9578  cantnflem1  9579  ssttrcl  9605  ttrcltr  9606  ttrclselem2  9616  r1sucg  9659  r0weon  9900  infxpenc2lem1  9907  fseqenlem1  9912  fseqenlem2  9913  dfac8alem  9917  ac5num  9924  acni2  9934  dfac4  10010  dfac2a  10018  dfacacn  10030  dfac12lem1  10032  ackbij1lem7  10113  ackbij2lem2  10127  ackbij2lem3  10128  cfsmolem  10158  fin23lem28  10228  fin23lem39  10238  isf32lem6  10246  isf32lem7  10247  isf32lem8  10248  fin1a2lem3  10290  itunifval  10304  itunisuc  10307  axdc2lem  10336  axdc3lem2  10339  axcclem  10345  zorn2lem1  10384  negiso  12099  infrenegsup  12102  uzval  12731  flval  13695  ceilval  13739  ceilval2  13741  monoord2  13937  seqf1olem2  13946  seqf1o  13947  seqdistr  13957  serle  13961  seqof  13963  swrdfv  14553  revval  14664  revfv  14667  wwlktovf1  14861  wwlktovfo  14862  sgnval  14992  cjval  15006  reval  15010  imval  15011  sqrtval  15141  absval  15142  limsupval  15378  limsupgval  15380  climmpt  15475  climle  15544  rlimdiv  15550  isercolllem1  15569  isercoll2  15573  caurcvg2  15582  fsumser  15634  isumadd  15671  fsumcnv  15677  fsumrev  15683  fsumshft  15684  iserabs  15719  cvgcmp  15720  cvgcmpce  15722  incexclem  15740  isumless  15749  divcnvshft  15759  supcvg  15760  harmonic  15763  trireciplem  15766  trirecip  15767  expcnv  15768  explecnv  15769  geolim  15774  geolim2  15775  geo2lim  15779  geomulcvg  15780  geoisum  15781  geoisumr  15782  geoisum1  15783  geoisum1c  15784  cvgrat  15787  mertenslem2  15789  mertens  15790  prodfdiv  15800  fprodser  15853  fprodshft  15880  fprodrev  15881  fprodcnv  15887  iprodmul  15907  bpolylem  15952  eftval  15980  efval  15983  efcvgfsum  15990  ege2le3  15994  eftlub  16015  eflegeo  16027  sinval  16028  cosval  16029  tanval  16034  eirrlem  16110  rpnnen2lem1  16120  rpnnen2lem2  16121  bitsfval  16331  bitsinv2  16351  bitsinv  16356  sadcf  16361  sadc0  16362  sadcp1  16363  smupf  16386  smup0  16387  smupp1  16388  qnumval  16645  qdenval  16646  phival  16675  crth  16686  phimullem  16687  eulerthlem2  16690  phisum  16699  odzval  16700  iserodd  16744  pcmpt  16801  prmreclem1  16825  prmreclem2  16826  prmreclem4  16828  prmreclem5  16829  prmreclem6  16830  1arithlem1  16832  1arithlem2  16833  vdwapfval  16880  vdwlem2  16891  vdwlem6  16895  vdwlem8  16897  vdwlem9  16898  ramub1lem2  16936  ramcl  16938  prmoval  16942  strfvnd  17093  topnval  17335  prdsplusgfval  17375  prdsmulrfval  17377  isacs  17554  acsfn  17562  homffval  17593  comfffval  17601  oppcval  17616  monfval  17636  oppcmon  17642  sectffval  17654  invffval  17662  isoval  17669  idfuval  17780  homafval  17933  arwval  17947  coafval  17968  yonedainv  18184  oduval  18191  pltfval  18232  lubfval  18251  lubval  18257  glbfval  18264  glbval  18270  p0val  18328  p1val  18329  ipoval  18433  plusffval  18551  grpidval  18566  issubmgm  18607  issubm  18708  prdspjmhm  18734  efmnd  18775  smndex1igid  18809  grpinvfval  18888  grpinvval  18890  grpsubfval  18893  grpsubfvalALT  18894  grplactval  18952  prdsinvlem  18959  mulgfval  18979  mulgfvalALT  18980  pwsmulg  19029  issubg  19036  isnsg  19065  cycsubmel  19110  cycsubgcl  19116  conjghm  19159  conjnmz  19162  cntrval  19229  cntzfval  19230  cntzval  19231  oppgval  19257  psgnfval  19410  psgnval  19417  odfval  19442  odval  19444  sylow1lem4  19511  pgpssslw  19524  sylow2blem3  19532  sylow3lem2  19538  lsmfval  19548  pj1fval  19604  efgval  19627  efgsval  19641  frgpval  19668  vrgpval  19677  mulgmhm  19737  mulgghm  19738  ablfaclem1  19997  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  20460  issubrg  20484  rgspnval  20525  rrgval  20610  fidomndrnglem  20685  issdrg  20701  abvfval  20723  abvtrivd  20745  staffval  20754  stafval  20755  scaffval  20811  lmodvsghm  20854  lssset  20864  lspfval  20904  islbs  21008  sraval  21107  rlmval  21123  2idlval  21186  lpival  21259  expmhm  21371  expghm  21410  mulgghm2  21411  mulgrhm  21412  zrhval  21442  zrhmulg  21444  zlmval  21450  chrval  21458  znval  21470  znzrhval  21481  evpmss  21521  psgnevpmb  21522  ip0l  21571  ipffval  21583  ocvfval  21601  ocvval  21602  cssval  21617  thlval  21630  pjfval  21641  pjval  21645  isobs  21655  prdsinvgd2  21677  uvcresum  21728  frlmup1  21733  frlmup2  21734  islinds  21744  islindf5  21774  aspval  21808  asclval  21815  psrmulval  21879  psrlidm  21897  psrridm  21898  psrascl  21914  mvrval  21917  mvrval2  21918  mplmonmul  21969  evlslem3  22013  evlslem1  22015  evlsval  22019  evlssca  22022  evlsvar  22023  psdmul  22079  psdmvr  22082  psr1val  22096  vr1val  22102  ply1val  22104  coe1fval  22116  coe1fv  22117  coe1tmmul2  22188  coe1tmmul  22189  coe1tmmul2fv  22190  coe1pwmulfv  22192  evls1val  22233  evl1fval  22241  evl1val  22242  mamulid  22354  mamurid  22355  mdetleib  22500  mdetleib1  22504  mdetunilem9  22533  mdetuni0  22534  mdetmul  22536  cpmidpmatlem1  22783  ordtval  23102  cnpval  23149  ptpjpre1  23484  ptpjopn  23525  dfac14  23531  upxp  23536  uptx  23538  hauseqlcld  23559  txlm  23561  xkoptsub  23567  xkoinjcn  23600  kqval  23639  xpstopnlem1  23722  fmval  23856  flfval  23903  ptcmplem2  23966  ptcmplem3  23967  symgtgp  24019  qustgpopn  24033  ussval  24172  iscfilu  24200  ispsmet  24217  ismet  24236  isxmet  24237  mopnval  24351  prdsxmslem2  24442  nmfval  24501  nmval  24502  nmoval  24628  metdsval  24761  divcnOLD  24782  divcn  24784  mulc1cncf  24823  icopnfhmeo  24866  iccpnfhmeo  24868  xrhmeo  24869  cnheiborlem  24878  evth  24883  evth2  24884  lebnumlem3  24887  isphtpy  24905  isphtpc  24918  pcofval  24935  pcovalg  24937  pco1  24940  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevcl  24950  pcorevlem  24951  pcorev2  24953  pi1xfrcnv  24982  cphnm  25118  tcphval  25143  tcphnmval  25154  cfilfval  25189  iscmet  25209  iscmet3lem3  25215  rrxval  25312  ehlval  25339  ivth2  25381  ovolval  25399  ovollb2lem  25414  ovolunlem1a  25422  ovolunlem1  25423  ovoliunlem1  25428  ovoliunlem2  25429  ovolicc1  25442  voliunlem1  25476  voliunlem2  25477  voliunlem3  25478  volsup  25482  ioorval  25500  uniioombllem3  25511  uniioombllem6  25514  volsup2  25531  volcn  25532  volivth  25533  vitalilem2  25535  vitalilem3  25536  vitalilem4  25537  vitali  25539  mbfmax  25575  mbfimaopnlem  25581  itg1val  25609  i1f1lem  25615  itg11  25617  itg1addlem4  25625  itg1mulc  25630  i1fres  25631  itg1climres  25640  mbfi1fseqlem2  25642  mbfi1fseqlem3  25643  mbfi1fseqlem6  25646  mbfi1flimlem  25648  mbfi1flim  25649  mbfmullem2  25650  itg2seq  25668  itg2uba  25669  itg2splitlem  25674  itg2monolem1  25676  itg2monolem2  25677  itg2monolem3  25678  itg2mono  25679  itg2i1fseqle  25680  itg2i1fseq  25681  itg2i1fseq2  25682  itg2addlem  25684  itg2cnlem1  25687  itg2cn  25689  limccnp2  25818  dvnff  25850  dvnp1  25852  cpnfval  25859  elcpn  25861  dvrec  25884  dvcnvlem  25905  dveflem  25908  dvef  25909  dvferm1  25914  dvferm2  25916  rolle  25919  dvlip  25923  dvlipcn  25924  dv11cn  25931  dvivthlem1  25938  dvivth  25940  lhop1lem  25943  ftc1lem1  25967  ftc1lem5  25972  ftc2  25976  itgsubstlem  25980  tdeglem3  25989  tdeglem4  25990  mdegval  25993  mdegmullem  26008  deg1fval  26010  deg1ldg  26022  deg1leb  26025  coe1mul3  26029  uc1pval  26070  mon1pval  26072  mon1pid  26084  q1pval  26085  r1pval  26088  ply1remlem  26095  ig1pval  26106  plyval  26123  elply2  26126  plyeq0lem  26140  coeval  26153  dgrval  26158  coeid2  26169  coemullem  26180  coemul  26182  elqaalem1  26252  elqaalem2  26253  elqaalem3  26254  iaa  26258  aareccl  26259  aannenlem1  26261  geolim3  26272  aaliou3lem1  26275  aaliou3lem2  26276  aaliou3lem5  26280  aaliou3lem6  26281  aaliou3lem7  26282  aaliou3  26284  tayl0  26294  taylthlem1  26306  taylthlem2  26307  taylthlem2OLD  26308  ulmshftlem  26323  ulmshft  26324  ulmuni  26326  ulmcau  26329  ulmdvlem1  26334  ulmdvlem3  26336  mtest  26338  mtestbdd  26339  mbfulm  26340  iblulm  26341  itgulm  26342  pserval  26344  pserval2  26345  radcnvlem1  26347  radcnvlem2  26348  dvradcnv  26355  pserulm  26356  pserdvlem2  26363  pserdv  26364  abelthlem1  26366  abelthlem3  26368  abelthlem4  26369  abelthlem5  26370  abelthlem6  26371  abelthlem7  26373  abelthlem8  26374  abelthlem9  26375  resinf1o  26470  efif1olem4  26479  eff1olem  26482  logcnlem5  26580  logtayllem  26593  logtayl  26594  logtaylsum  26595  logtayl2  26596  logccv  26597  asinval  26817  acosval  26818  atanval  26819  atantayl  26872  leibpilem2  26876  leibpi  26877  leibpisum  26878  log2cnv  26879  log2tlbnd  26880  areaval  26899  efrlim  26904  efrlimOLD  26905  dfef2  26906  amgmlem  26925  emcllem2  26932  emcllem3  26933  emcllem4  26934  emcllem5  26935  emcllem6  26936  emcllem7  26937  zetacvg  26950  lgamgulmlem4  26967  lgamgulmlem5  26968  lgamgulm2  26971  lgamcvglem  26975  igamval  26982  lgamcvg2  26990  gamcvg2lem  26994  ftalem7  27014  basellem2  27017  basellem3  27018  basellem4  27019  basellem5  27020  basellem6  27021  basellem8  27023  basellem9  27024  chtval  27045  vmaval  27048  chpval  27057  ppival  27062  muval  27067  prmorcht  27113  sqff1o  27117  dvdsflsumcom  27123  musum  27126  muinv  27128  sgmppw  27133  fsumvma  27149  pclogsum  27151  dchrfi  27191  bposlem5  27224  bposlem7  27226  bposlem8  27227  bposlem9  27228  lgsfval  27238  lgsdir  27268  lgsdilem2  27269  lgsdi  27270  lgsne0  27271  lgsqrlem2  27283  lgsqrlem4  27285  lgseisenlem2  27312  dchrmusum2  27430  dchrvmasumlem1  27431  dchrvmasumiflem1  27437  dchrvmaeq0  27440  dchrisum0fval  27441  dchrisum0re  27449  mulog2sumlem1  27470  pntrval  27498  pntsval  27508  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntlem3  27545  abvcxp  27551  padicfval  27552  padicval  27553  padicabv  27566  ostth1  27569  ostth2  27573  ostth3  27574  nosupfv  27643  noinffv  27658  newval  27794  leftval  27802  rightval  27803  iscgrg  28488  legval  28560  ishpg  28735  iscgra  28785  isinag  28814  isleag  28823  iseqlg  28843  ttgval  28851  elee  28870  axsegconlem1  28893  axsegconlem9  28901  axsegconlem10  28902  axpasch  28917  axlowdimlem15  28932  axlowdim  28937  axeuclidlem  28938  axcontlem2  28941  eengv  28955  vtxval  28976  iedgval  28977  edgval  29025  vtxdgval  29445  wwlksnextinj  29875  wwlksnextsurj  29876  clwwlkfv  30023  clwwlknonmpo  30064  fusgreg2wsplem  30308  fusgreghash2wsp  30313  numclwwlk1lem2fv  30331  gidval  30487  grpoinvval  30498  bafval  30579  imsval  30660  dipfval  30677  sspval  30698  nmooval  30738  hmoval  30785  ipasslem8  30812  ipasslem9  30813  ipblnfi  30830  ubthlem2  30846  htthlem  30892  normval  31099  ocval  31255  occllem  31278  hsupval  31309  pjhfval  31371  pjhval  31372  chscllem2  31613  chscllem3  31614  hosval  31715  homval  31716  hodval  31717  hfsval  31718  hfmval  31719  brafval  31918  braval  31919  kbval  31929  eigvalval  31935  cnlnadjlem1  32042  nmopadjlei  32063  hmopidmchi  32126  strlem2  32226  hstrlem2  32234  cdj3lem2  32410  ofpreima  32642  psgnfzto1stlem  33064  evpmval  33109  altgnsg  33113  inftmrel  33144  isinftm  33145  qusker  33309  qusvscpbl  33311  qusvsval  33312  mxidlval  33421  idlsrgval  33463  dimval  33608  dimvalfi  33609  smatfval  33803  lmatval  33821  locfinreflem  33848  rspecval  33872  rmulccn  33936  xrmulc1cn  33938  xrge0iifcv  33942  xrge0iifiso  33943  xrge0iifhom  33945  xrge0iif1  33946  qqhval  33980  rrhval  34004  xrhval  34026  ddeval1  34242  ddeval0  34243  sxbrsigalem0  34279  sxbrsigalem3  34280  eulerpartlemgv  34381  rrvmbfm  34450  dstrvval  34479  coinflippv  34492  ballotlem2  34497  ballotlemfval  34498  ballotlemi  34509  ballotlemsval  34517  ballotlemrval  34526  ballotth  34546  plymulx  34556  signstfv  34571  signsvvfval  34586  onvf1odlem3  35137  derangval  35199  subfacval  35205  erdszelem3  35225  erdszelem9  35231  erdszelem10  35232  txpconn  35264  indispconn  35266  cvxpconn  35274  cvmlift2lem2  35336  cvmlift2lem3  35337  cvmlift2lem7  35341  cvmliftphtlem  35349  cvmlift3lem4  35354  snmlfval  35362  snmlval  35363  gonafv  35382  mvtval  35532  mrsubffval  35539  mrsubcv  35542  mrsubrn  35545  elmrsubrn  35552  msubffval  35555  mvhval  35566  mpstval  35567  mstaval  35576  mclsval  35595  mppsval  35604  sinccvglem  35704  circum  35706  divcnvlin  35765  iprodefisum  35773  iprodgam  35774  faclimlem1  35775  faclimlem2  35776  faclim  35778  iprodfac  35779  faclim2  35780  dfrdg2  35828  findabrcl  36487  dnival  36504  bj-evalval  37108  bj-inftyexpitaudisj  37238  bj-inftyexpiinv  37241  bj-inftyexpidisj  37243  curfv  37639  finixpnum  37644  poimirlem16  37675  poimir  37692  broucube  37693  mblfinlem2  37697  voliunnfl  37703  volsupnfl  37704  itg2addnclem  37710  itg2addnclem3  37712  ftc1cnnc  37731  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anc  37740  ftc2nc  37741  fvopabf4g  37761  sdclem2  37781  fdc  37784  lmclim2  37797  geomcau  37798  istotbnd  37808  isbnd  37819  prdsbnd2  37834  heiborlem6  37855  heiborlem7  37856  heiborlem8  37857  rrnval  37866  rrncmslem  37871  idlval  38052  pridlval  38072  maxidlval  38078  lshpset  39016  lsatset  39028  lcvfbr  39058  lflset  39097  lflnegcl  39113  lshpkrlem1  39148  lshpkrlem2  39149  lshpkrlem3  39150  ldualset  39163  cmtfvalN  39248  cvrfval  39306  pats  39323  llnset  39543  lplnset  39567  lvolset  39610  lineset  39776  pointsetN  39779  psubspset  39782  pmapval  39795  paddfval  39835  pclfvalN  39927  polfvalN  39942  polvalN  39943  psubclsetN  39974  watvalN  40031  lhpset  40033  lautset  40120  pautsetN  40136  ldilset  40147  ltrnset  40156  dilsetN  40191  trnsetN  40194  trlset  40199  trlval  40200  tgrpset  40783  tendoset  40797  tendo02  40825  erngset  40838  erngset-rN  40846  cdlemksv  40882  dvaset  41043  dvaplusgv  41048  diafval  41069  diaval  41070  dvhset  41119  cdlemm10N  41156  docafvalN  41160  djafvalN  41172  dibfval  41179  dibval  41180  dicfval  41213  dicval  41214  dihval  41270  dochfval  41388  djhfval  41435  dochfl1  41514  lpolsetN  41520  lcdval  41627  mapdhval  41762  hvmapfval  41797  hdmap1fval  41834  fimgmcyc  42566  prjspval  42635  isnacs  42736  mzpclval  42757  mzpsubst  42780  mzprename  42781  mzpcompact2lem  42783  eldiophb  42789  diophrw  42791  eldioph2  42794  diophin  42804  diophun  42805  diophren  42845  pell1qrval  42878  pell14qrval  42880  pell1234qrval  42882  pellfundval  42912  rmxypairf1o  42943  rmxyval  42947  mzpcong  43004  pw2f1ocnv  43069  dnnumch1  43076  dfac11  43094  hbtlem1  43155  hbtlem7  43157  elmnc  43168  dgraaval  43176  mpaaval  43183  itgoval  43193  flcidc  43202  mendval  43211  cytpval  43234  cantnfub  43353  cantnfresb  43356  tfsconcatrev  43380  elcnvlem  43633  comptiunov2i  43738  dftrcl3  43752  trclfvcom  43755  cnvtrclfv  43756  cotrcltrcl  43757  trclimalb2  43758  trclfvdecomr  43760  dfrtrcl3  43765  dfrtrcl4  43770  clsk1indlem0  44073  clsk1indlem2  44074  clsk1indlem3  44075  clsk1indlem4  44076  clsk1indlem1  44077  k0004val  44182  lhe4.4ex1a  44361  addrfv  44500  subrfv  44501  mulvfv  44502  monoord2xrv  45520  sumnnodd  45669  liminfgval  45799  ioodvbdlimc2lem  45971  itgsin0pilem1  45987  stoweidlem55  46092  wallispilem1  46102  wallispilem2  46103  wallispilem4  46105  wallispi2lem1  46108  wallispi2lem2  46109  dirkerval  46128  fourierdlem2  46146  fourierdlem3  46147  fourierdlem29  46173  fourierdlem62  46205  fourierdlem80  46223  fourierdlem103  46246  fourierdlem104  46247  fourierswlem  46267  fouriersw  46268  iundjiunlem  46496  carageniuncllem2  46559  0ome  46566  hoidmv1le  46631  hoidmvlelem3  46634  smflimsuplem7  46863  iccpval  47445  fppr  47756  bigoval  48580  ackval0  48711  ackval41a  48725  eenglngeehlnm  48770  oppcinito  49266  oppctermo  49267  dfinito4  49532  prstcval  49582  mndtcval  49610  setc1onsubc  49633  lmdfval2  49686  cmdfval2  49687  vsetrec  49734  onsetreclem1  49736  elpglem3  49744  pgindnf  49747  sinhval-named  49767  coshval-named  49768  tanhval-named  49769  secval  49778  cscval  49779  cotval  49780  aacllem  49832