Theorem fvmpt 6934

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438   ↦ cmpt 5176  ‘cfv 6486

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmptex  6948  fvmptrabfv  6966  mptfvmpt  7168  fvmptopab  7408  ofval  7628  caofinvl  7649  fvresex  7902  1stval  7933  2ndval  7934  reldm  7986  curry1val  8045  curry2val  8049  fsplitfpar  8058  fnwelem  8071  brtpos2  8172  onovuni  8272  tz7.44-1  8335  oasuc  8449  oesuclem  8450  omsuc  8451  onasuc  8453  onmsuc  8454  fsetfocdm  8795  fvmptmap  8815  xpcomco  8991  unxpdomlem1  9155  unfilem2  9213  ordtypelem3  9431  ixpiunwdom  9501  inf3lema  9539  noinfep  9575  cantnfval  9583  cantnflem1d  9603  cantnflem1  9604  ssttrcl  9630  ttrcltr  9631  ttrclselem2  9641  r1sucg  9684  r0weon  9925  infxpenc2lem1  9932  fseqenlem1  9937  fseqenlem2  9938  dfac8alem  9942  ac5num  9949  acni2  9959  dfac4  10035  dfac2a  10043  dfacacn  10055  dfac12lem1  10057  ackbij1lem7  10138  ackbij2lem2  10152  ackbij2lem3  10153  cfsmolem  10183  fin23lem28  10253  fin23lem39  10263  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  fin1a2lem3  10315  itunifval  10329  itunisuc  10332  axdc2lem  10361  axdc3lem2  10364  axcclem  10370  zorn2lem1  10409  negiso  12123  infrenegsup  12126  uzval  12755  flval  13716  ceilval  13760  ceilval2  13762  monoord2  13958  seqf1olem2  13967  seqf1o  13968  seqdistr  13978  serle  13982  seqof  13984  swrdfv  14573  revval  14684  revfv  14687  wwlktovf1  14882  wwlktovfo  14883  sgnval  15013  cjval  15027  reval  15031  imval  15032  sqrtval  15162  absval  15163  limsupval  15399  limsupgval  15401  climmpt  15496  climle  15565  rlimdiv  15571  isercolllem1  15590  isercoll2  15594  caurcvg2  15603  fsumser  15655  isumadd  15692  fsumcnv  15698  fsumrev  15704  fsumshft  15705  iserabs  15740  cvgcmp  15741  cvgcmpce  15743  incexclem  15761  isumless  15770  divcnvshft  15780  supcvg  15781  harmonic  15784  trireciplem  15787  trirecip  15788  expcnv  15789  explecnv  15790  geolim  15795  geolim2  15796  geo2lim  15800  geomulcvg  15801  geoisum  15802  geoisumr  15803  geoisum1  15804  geoisum1c  15805  cvgrat  15808  mertenslem2  15810  mertens  15811  prodfdiv  15821  fprodser  15874  fprodshft  15901  fprodrev  15902  fprodcnv  15908  iprodmul  15928  bpolylem  15973  eftval  16001  efval  16004  efcvgfsum  16011  ege2le3  16015  eftlub  16036  eflegeo  16048  sinval  16049  cosval  16050  tanval  16055  eirrlem  16131  rpnnen2lem1  16141  rpnnen2lem2  16142  bitsfval  16352  bitsinv2  16372  bitsinv  16377  sadcf  16382  sadc0  16383  sadcp1  16384  smupf  16407  smup0  16408  smupp1  16409  qnumval  16666  qdenval  16667  phival  16696  crth  16707  phimullem  16708  eulerthlem2  16711  phisum  16720  odzval  16721  iserodd  16765  pcmpt  16822  prmreclem1  16846  prmreclem2  16847  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arithlem1  16853  1arithlem2  16854  vdwapfval  16901  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  ramub1lem2  16957  ramcl  16959  prmoval  16963  strfvnd  17114  topnval  17356  prdsplusgfval  17396  prdsmulrfval  17398  isacs  17575  acsfn  17583  homffval  17614  comfffval  17622  oppcval  17637  monfval  17657  oppcmon  17663  sectffval  17675  invffval  17683  isoval  17690  idfuval  17801  homafval  17954  arwval  17968  coafval  17989  yonedainv  18205  oduval  18212  pltfval  18253  lubfval  18272  lubval  18278  glbfval  18285  glbval  18291  p0val  18349  p1val  18350  ipoval  18454  plusffval  18538  grpidval  18553  issubmgm  18594  issubm  18695  prdspjmhm  18721  efmnd  18762  smndex1igid  18796  grpinvfval  18875  grpinvval  18877  grpsubfval  18880  grpsubfvalALT  18881  grplactval  18939  prdsinvlem  18946  mulgfval  18966  mulgfvalALT  18967  pwsmulg  19016  issubg  19023  isnsg  19052  cycsubmel  19097  cycsubgcl  19103  conjghm  19146  conjnmz  19149  cntrval  19216  cntzfval  19217  cntzval  19218  oppgval  19244  psgnfval  19397  psgnval  19404  odfval  19429  odval  19431  sylow1lem4  19498  pgpssslw  19511  sylow2blem3  19519  sylow3lem2  19525  lsmfval  19535  pj1fval  19591  efgval  19614  efgsval  19628  frgpval  19655  vrgpval  19664  mulgmhm  19724  mulgghm  19725  ablfaclem1  19984  mgpval  20046  srglmhm  20124  srgrmhm  20125  ringlghm  20215  ringrghm  20216  pwspjmhmmgpd  20231  pwsexpg  20232  opprval  20241  dvdsrval  20264  isunit  20276  invrfval  20292  dvrfval  20305  isirred  20322  issubrng  20450  issubrg  20474  rgspnval  20515  rrgval  20600  fidomndrnglem  20675  issdrg  20691  abvfval  20713  abvtrivd  20735  staffval  20744  stafval  20745  scaffval  20801  lmodvsghm  20844  lssset  20854  lspfval  20894  islbs  20998  sraval  21097  rlmval  21113  2idlval  21176  lpival  21249  expmhm  21361  expghm  21400  mulgghm2  21401  mulgrhm  21402  zrhval  21432  zrhmulg  21434  zlmval  21440  chrval  21448  znval  21460  znzrhval  21471  evpmss  21511  psgnevpmb  21512  ip0l  21561  ipffval  21573  ocvfval  21591  ocvval  21592  cssval  21607  thlval  21620  pjfval  21631  pjval  21635  isobs  21645  prdsinvgd2  21667  uvcresum  21718  frlmup1  21723  frlmup2  21724  islinds  21734  islindf5  21764  aspval  21798  asclval  21805  psrmulval  21869  psrlidm  21887  psrridm  21888  psrascl  21904  mvrval  21907  mvrval2  21908  mplmonmul  21959  evlslem3  22003  evlslem1  22005  evlsval  22009  evlssca  22012  evlsvar  22013  psdmul  22069  psdmvr  22072  psr1val  22086  vr1val  22092  ply1val  22094  coe1fval  22106  coe1fv  22107  coe1tmmul2  22178  coe1tmmul  22179  coe1tmmul2fv  22180  coe1pwmulfv  22182  evls1val  22223  evl1fval  22231  evl1val  22232  mamulid  22344  mamurid  22345  mdetleib  22490  mdetleib1  22494  mdetunilem9  22523  mdetuni0  22524  mdetmul  22526  cpmidpmatlem1  22773  ordtval  23092  cnpval  23139  ptpjpre1  23474  ptpjopn  23515  dfac14  23521  upxp  23526  uptx  23528  hauseqlcld  23549  txlm  23551  xkoptsub  23557  xkoinjcn  23590  kqval  23629  xpstopnlem1  23712  fmval  23846  flfval  23893  ptcmplem2  23956  ptcmplem3  23957  symgtgp  24009  qustgpopn  24023  ussval  24163  iscfilu  24191  ispsmet  24208  ismet  24227  isxmet  24228  mopnval  24342  prdsxmslem2  24433  nmfval  24492  nmval  24493  nmoval  24619  metdsval  24752  divcnOLD  24773  divcn  24775  mulc1cncf  24814  icopnfhmeo  24857  iccpnfhmeo  24859  xrhmeo  24860  cnheiborlem  24869  evth  24874  evth2  24875  lebnumlem3  24878  isphtpy  24896  isphtpc  24909  pcofval  24926  pcovalg  24928  pco1  24931  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevcl  24941  pcorevlem  24942  pcorev2  24944  pi1xfrcnv  24973  cphnm  25109  tcphval  25134  tcphnmval  25145  cfilfval  25180  iscmet  25200  iscmet3lem3  25206  rrxval  25303  ehlval  25330  ivth2  25372  ovolval  25390  ovollb2lem  25405  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliunlem2  25420  ovolicc1  25433  voliunlem1  25467  voliunlem2  25468  voliunlem3  25469  volsup  25473  ioorval  25491  uniioombllem3  25502  uniioombllem6  25505  volsup2  25522  volcn  25523  volivth  25524  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  vitali  25530  mbfmax  25566  mbfimaopnlem  25572  itg1val  25600  i1f1lem  25606  itg11  25608  itg1addlem4  25616  itg1mulc  25621  i1fres  25622  itg1climres  25631  mbfi1fseqlem2  25633  mbfi1fseqlem3  25634  mbfi1fseqlem6  25637  mbfi1flimlem  25639  mbfi1flim  25640  mbfmullem2  25641  itg2seq  25659  itg2uba  25660  itg2splitlem  25665  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  itg2i1fseqle  25671  itg2i1fseq  25672  itg2i1fseq2  25673  itg2addlem  25675  itg2cnlem1  25678  itg2cn  25680  limccnp2  25809  dvnff  25841  dvnp1  25843  cpnfval  25850  elcpn  25852  dvrec  25875  dvcnvlem  25896  dveflem  25899  dvef  25900  dvferm1  25905  dvferm2  25907  rolle  25910  dvlip  25914  dvlipcn  25915  dv11cn  25922  dvivthlem1  25929  dvivth  25931  lhop1lem  25934  ftc1lem1  25958  ftc1lem5  25963  ftc2  25967  itgsubstlem  25971  tdeglem3  25980  tdeglem4  25981  mdegval  25984  mdegmullem  25999  deg1fval  26001  deg1ldg  26013  deg1leb  26016  coe1mul3  26020  uc1pval  26061  mon1pval  26063  mon1pid  26075  q1pval  26076  r1pval  26079  ply1remlem  26086  ig1pval  26097  plyval  26114  elply2  26117  plyeq0lem  26131  coeval  26144  dgrval  26149  coeid2  26160  coemullem  26171  coemul  26173  elqaalem1  26243  elqaalem2  26244  elqaalem3  26245  iaa  26249  aareccl  26250  aannenlem1  26252  geolim3  26263  aaliou3lem1  26266  aaliou3lem2  26267  aaliou3lem5  26271  aaliou3lem6  26272  aaliou3lem7  26273  aaliou3  26275  tayl0  26285  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmshftlem  26314  ulmshft  26315  ulmuni  26317  ulmcau  26320  ulmdvlem1  26325  ulmdvlem3  26327  mtest  26329  mtestbdd  26330  mbfulm  26331  iblulm  26332  itgulm  26333  pserval  26335  pserval2  26336  radcnvlem1  26338  radcnvlem2  26339  dvradcnv  26346  pserulm  26347  pserdvlem2  26354  pserdv  26355  abelthlem1  26357  abelthlem3  26359  abelthlem4  26360  abelthlem5  26361  abelthlem6  26362  abelthlem7  26364  abelthlem8  26365  abelthlem9  26366  resinf1o  26461  efif1olem4  26470  eff1olem  26473  logcnlem5  26571  logtayllem  26584  logtayl  26585  logtaylsum  26586  logtayl2  26587  logccv  26588  asinval  26808  acosval  26809  atanval  26810  atantayl  26863  leibpilem2  26867  leibpi  26868  leibpisum  26869  log2cnv  26870  log2tlbnd  26871  areaval  26890  efrlim  26895  efrlimOLD  26896  dfef2  26897  amgmlem  26916  emcllem2  26923  emcllem3  26924  emcllem4  26925  emcllem5  26926  emcllem6  26927  emcllem7  26928  zetacvg  26941  lgamgulmlem4  26958  lgamgulmlem5  26959  lgamgulm2  26962  lgamcvglem  26966  igamval  26973  lgamcvg2  26981  gamcvg2lem  26985  ftalem7  27005  basellem2  27008  basellem3  27009  basellem4  27010  basellem5  27011  basellem6  27012  basellem8  27014  basellem9  27015  chtval  27036  vmaval  27039  chpval  27048  ppival  27053  muval  27058  prmorcht  27104  sqff1o  27108  dvdsflsumcom  27114  musum  27117  muinv  27119  sgmppw  27124  fsumvma  27140  pclogsum  27142  dchrfi  27182  bposlem5  27215  bposlem7  27217  bposlem8  27218  bposlem9  27219  lgsfval  27229  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  lgsqrlem2  27274  lgsqrlem4  27276  lgseisenlem2  27303  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasumiflem1  27428  dchrvmaeq0  27431  dchrisum0fval  27432  dchrisum0re  27440  mulog2sumlem1  27461  pntrval  27489  pntsval  27499  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntlem3  27536  abvcxp  27542  padicfval  27543  padicval  27544  padicabv  27557  ostth1  27560  ostth2  27564  ostth3  27565  nosupfv  27634  noinffv  27649  newval  27783  leftval  27791  rightval  27792  iscgrg  28475  legval  28547  ishpg  28722  iscgra  28772  isinag  28801  isleag  28810  iseqlg  28830  ttgval  28838  elee  28857  axsegconlem1  28880  axsegconlem9  28888  axsegconlem10  28889  axpasch  28904  axlowdimlem15  28919  axlowdim  28924  axeuclidlem  28925  axcontlem2  28928  eengv  28942  vtxval  28963  iedgval  28964  edgval  29012  vtxdgval  29432  wwlksnextinj  29862  wwlksnextsurj  29863  clwwlkfv  30010  clwwlknonmpo  30051  fusgreg2wsplem  30295  fusgreghash2wsp  30300  numclwwlk1lem2fv  30318  gidval  30474  grpoinvval  30485  bafval  30566  imsval  30647  dipfval  30664  sspval  30685  nmooval  30725  hmoval  30772  ipasslem8  30799  ipasslem9  30800  ipblnfi  30817  ubthlem2  30833  htthlem  30879  normval  31086  ocval  31242  occllem  31265  hsupval  31296  pjhfval  31358  pjhval  31359  chscllem2  31600  chscllem3  31601  hosval  31702  homval  31703  hodval  31704  hfsval  31705  hfmval  31706  brafval  31905  braval  31906  kbval  31916  eigvalval  31922  cnlnadjlem1  32029  nmopadjlei  32050  hmopidmchi  32113  strlem2  32213  hstrlem2  32221  cdj3lem2  32397  ofpreima  32622  psgnfzto1stlem  33055  evpmval  33100  altgnsg  33104  inftmrel  33132  isinftm  33133  qusker  33296  qusvscpbl  33298  qusvsval  33299  mxidlval  33408  idlsrgval  33450  dimval  33572  dimvalfi  33573  smatfval  33761  lmatval  33779  locfinreflem  33806  rspecval  33830  rmulccn  33894  xrmulc1cn  33896  xrge0iifcv  33900  xrge0iifiso  33901  xrge0iifhom  33903  xrge0iif1  33904  qqhval  33938  rrhval  33962  xrhval  33984  ddeval1  34200  ddeval0  34201  sxbrsigalem0  34238  sxbrsigalem3  34239  eulerpartlemgv  34340  rrvmbfm  34409  dstrvval  34438  coinflippv  34451  ballotlem2  34456  ballotlemfval  34457  ballotlemi  34468  ballotlemsval  34476  ballotlemrval  34485  ballotth  34505  plymulx  34515  signstfv  34530  signsvvfval  34545  onvf1odlem3  35077  derangval  35139  subfacval  35145  erdszelem3  35165  erdszelem9  35171  erdszelem10  35172  txpconn  35204  indispconn  35206  cvxpconn  35214  cvmlift2lem2  35276  cvmlift2lem3  35277  cvmlift2lem7  35281  cvmliftphtlem  35289  cvmlift3lem4  35294  snmlfval  35302  snmlval  35303  gonafv  35322  mvtval  35472  mrsubffval  35479  mrsubcv  35482  mrsubrn  35485  elmrsubrn  35492  msubffval  35495  mvhval  35506  mpstval  35507  mstaval  35516  mclsval  35535  mppsval  35544  sinccvglem  35644  circum  35646  divcnvlin  35705  iprodefisum  35713  iprodgam  35714  faclimlem1  35715  faclimlem2  35716  faclim  35718  iprodfac  35719  faclim2  35720  dfrdg2  35768  findabrcl  36427  dnival  36444  bj-evalval  37048  bj-inftyexpitaudisj  37178  bj-inftyexpiinv  37181  bj-inftyexpidisj  37183  curfv  37579  finixpnum  37584  poimirlem16  37615  poimir  37632  broucube  37633  mblfinlem2  37637  voliunnfl  37643  volsupnfl  37644  itg2addnclem  37650  itg2addnclem3  37652  ftc1cnnc  37671  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anc  37680  ftc2nc  37681  fvopabf4g  37701  sdclem2  37721  fdc  37724  lmclim2  37737  geomcau  37738  istotbnd  37748  isbnd  37759  prdsbnd2  37774  heiborlem6  37795  heiborlem7  37796  heiborlem8  37797  rrnval  37806  rrncmslem  37811  idlval  37992  pridlval  38012  maxidlval  38018  lshpset  38956  lsatset  38968  lcvfbr  38998  lflset  39037  lflnegcl  39053  lshpkrlem1  39088  lshpkrlem2  39089  lshpkrlem3  39090  ldualset  39103  cmtfvalN  39188  cvrfval  39246  pats  39263  llnset  39484  lplnset  39508  lvolset  39551  lineset  39717  pointsetN  39720  psubspset  39723  pmapval  39736  paddfval  39776  pclfvalN  39868  polfvalN  39883  polvalN  39884  psubclsetN  39915  watvalN  39972  lhpset  39974  lautset  40061  pautsetN  40077  ldilset  40088  ltrnset  40097  dilsetN  40132  trnsetN  40135  trlset  40140  trlval  40141  tgrpset  40724  tendoset  40738  tendo02  40766  erngset  40779  erngset-rN  40787  cdlemksv  40823  dvaset  40984  dvaplusgv  40989  diafval  41010  diaval  41011  dvhset  41060  cdlemm10N  41097  docafvalN  41101  djafvalN  41113  dibfval  41120  dibval  41121  dicfval  41154  dicval  41155  dihval  41211  dochfval  41329  djhfval  41376  dochfl1  41455  lpolsetN  41461  lcdval  41568  mapdhval  41703  hvmapfval  41738  hdmap1fval  41775  fimgmcyc  42507  prjspval  42576  isnacs  42677  mzpclval  42698  mzpsubst  42721  mzprename  42722  mzpcompact2lem  42724  eldiophb  42730  diophrw  42732  eldioph2  42735  diophin  42745  diophun  42746  diophren  42786  pell1qrval  42819  pell14qrval  42821  pell1234qrval  42823  pellfundval  42853  rmxypairf1o  42884  rmxyval  42888  mzpcong  42945  pw2f1ocnv  43010  dnnumch1  43017  dfac11  43035  hbtlem1  43096  hbtlem7  43098  elmnc  43109  dgraaval  43117  mpaaval  43124  itgoval  43134  flcidc  43143  mendval  43152  cytpval  43175  cantnfub  43294  cantnfresb  43297  tfsconcatrev  43321  elcnvlem  43574  comptiunov2i  43679  dftrcl3  43693  trclfvcom  43696  cnvtrclfv  43697  cotrcltrcl  43698  trclimalb2  43699  trclfvdecomr  43701  dfrtrcl3  43706  dfrtrcl4  43711  clsk1indlem0  44014  clsk1indlem2  44015  clsk1indlem3  44016  clsk1indlem4  44017  clsk1indlem1  44018  k0004val  44123  lhe4.4ex1a  44302  addrfv  44442  subrfv  44443  mulvfv  44444  monoord2xrv  45463  sumnnodd  45612  liminfgval  45744  ioodvbdlimc2lem  45916  itgsin0pilem1  45932  stoweidlem55  46037  wallispilem1  46047  wallispilem2  46048  wallispilem4  46050  wallispi2lem1  46053  wallispi2lem2  46054  dirkerval  46073  fourierdlem2  46091  fourierdlem3  46092  fourierdlem29  46118  fourierdlem62  46150  fourierdlem80  46168  fourierdlem103  46191  fourierdlem104  46192  fourierswlem  46212  fouriersw  46213  iundjiunlem  46441  carageniuncllem2  46504  0ome  46511  hoidmv1le  46576  hoidmvlelem3  46579  smflimsuplem7  46808  iccpval  47400  fppr  47711  bigoval  48535  ackval0  48666  ackval41a  48680  eenglngeehlnm  48725  oppcinito  49221  oppctermo  49222  dfinito4  49487  prstcval  49537  mndtcval  49565  setc1onsubc  49588  lmdfval2  49641  cmdfval2  49642  vsetrec  49689  onsetreclem1  49691  elpglem3  49699  pgindnf  49702  sinhval-named  49722  coshval-named  49723  tanhval-named  49724  secval  49733  cscval  49734  cotval  49735  aacllem  49787