Theorem fvmpt 6985

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ↦ cmpt 5201  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538

This theorem is referenced by:  fvmptex  6999  fvmptrabfv  7017  mptfvmpt  7219  fvmptopab  7459  ofval  7680  caofinvl  7701  fvresex  7956  1stval  7988  2ndval  7989  reldm  8041  curry1val  8102  curry2val  8106  fsplitfpar  8115  fnwelem  8128  brtpos2  8229  onovuni  8354  tz7.44-1  8418  oasuc  8534  oesuclem  8535  omsuc  8536  onasuc  8538  onmsuc  8539  fsetfocdm  8873  fvmptmap  8893  xpcomco  9074  unxpdomlem1  9256  unfilem2  9314  ordtypelem3  9532  ixpiunwdom  9602  inf3lema  9636  noinfep  9672  cantnfval  9680  cantnflem1d  9700  cantnflem1  9701  ssttrcl  9727  ttrcltr  9728  ttrclselem2  9738  r1sucg  9781  r0weon  10024  infxpenc2lem1  10031  fseqenlem1  10036  fseqenlem2  10037  dfac8alem  10041  ac5num  10048  acni2  10058  dfac4  10134  dfac2a  10142  dfacacn  10154  dfac12lem1  10156  ackbij1lem7  10237  ackbij2lem2  10251  ackbij2lem3  10252  cfsmolem  10282  fin23lem28  10352  fin23lem39  10362  isf32lem6  10370  isf32lem7  10371  isf32lem8  10372  fin1a2lem3  10414  itunifval  10428  itunisuc  10431  axdc2lem  10460  axdc3lem2  10463  axcclem  10469  zorn2lem1  10508  negiso  12220  infrenegsup  12223  uzval  12852  flval  13809  ceilval  13853  ceilval2  13855  monoord2  14049  seqf1olem2  14058  seqf1o  14059  seqdistr  14069  serle  14073  seqof  14075  swrdfv  14664  revval  14776  revfv  14779  wwlktovf1  14974  wwlktovfo  14975  sgnval  15105  cjval  15119  reval  15123  imval  15124  sqrtval  15254  absval  15255  limsupval  15488  limsupgval  15490  climmpt  15585  climle  15654  rlimdiv  15660  isercolllem1  15679  isercoll2  15683  caurcvg2  15692  fsumser  15744  isumadd  15781  fsumcnv  15787  fsumrev  15793  fsumshft  15794  iserabs  15829  cvgcmp  15830  cvgcmpce  15832  incexclem  15850  isumless  15859  divcnvshft  15869  supcvg  15870  harmonic  15873  trireciplem  15876  trirecip  15877  expcnv  15878  explecnv  15879  geolim  15884  geolim2  15885  geo2lim  15889  geomulcvg  15890  geoisum  15891  geoisumr  15892  geoisum1  15893  geoisum1c  15894  cvgrat  15897  mertenslem2  15899  mertens  15900  prodfdiv  15910  fprodser  15963  fprodshft  15990  fprodrev  15991  fprodcnv  15997  iprodmul  16017  bpolylem  16062  eftval  16090  efval  16093  efcvgfsum  16100  ege2le3  16104  eftlub  16125  eflegeo  16137  sinval  16138  cosval  16139  tanval  16144  eirrlem  16220  rpnnen2lem1  16230  rpnnen2lem2  16231  bitsfval  16440  bitsinv2  16460  bitsinv  16465  sadcf  16470  sadc0  16471  sadcp1  16472  smupf  16495  smup0  16496  smupp1  16497  qnumval  16754  qdenval  16755  phival  16784  crth  16795  phimullem  16796  eulerthlem2  16799  phisum  16808  odzval  16809  iserodd  16853  pcmpt  16910  prmreclem1  16934  prmreclem2  16935  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  1arithlem1  16941  1arithlem2  16942  vdwapfval  16989  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  ramub1lem2  17045  ramcl  17047  prmoval  17051  strfvnd  17202  topnval  17446  prdsplusgfval  17486  prdsmulrfval  17488  isacs  17661  acsfn  17669  homffval  17700  comfffval  17708  oppcval  17723  monfval  17743  oppcmon  17749  sectffval  17761  invffval  17769  isoval  17776  idfuval  17887  homafval  18040  arwval  18054  coafval  18075  yonedainv  18291  oduval  18298  pltfval  18339  lubfval  18358  lubval  18364  glbfval  18371  glbval  18377  p0val  18435  p1val  18436  ipoval  18538  plusffval  18622  grpidval  18637  issubmgm  18678  issubm  18779  prdspjmhm  18805  efmnd  18846  smndex1igid  18880  grpinvfval  18959  grpinvval  18961  grpsubfval  18964  grpsubfvalALT  18965  grplactval  19023  prdsinvlem  19030  mulgfval  19050  mulgfvalALT  19051  pwsmulg  19100  issubg  19107  isnsg  19136  cycsubmel  19181  cycsubgcl  19187  conjghm  19230  conjnmz  19233  cntrval  19300  cntzfval  19301  cntzval  19302  oppgval  19328  psgnfval  19479  psgnval  19486  odfval  19511  odval  19513  sylow1lem4  19580  pgpssslw  19593  sylow2blem3  19601  sylow3lem2  19607  lsmfval  19617  pj1fval  19673  efgval  19696  efgsval  19710  frgpval  19737  vrgpval  19746  mulgmhm  19806  mulgghm  19807  ablfaclem1  20066  mgpval  20101  srglmhm  20179  srgrmhm  20180  ringlghm  20270  ringrghm  20271  pwspjmhmmgpd  20286  pwsexpg  20287  opprval  20296  dvdsrval  20319  isunit  20331  invrfval  20347  dvrfval  20360  isirred  20377  issubrng  20505  issubrg  20529  rgspnval  20570  rrgval  20655  fidomndrnglem  20730  issdrg  20746  abvfval  20768  abvtrivd  20790  staffval  20799  stafval  20800  scaffval  20835  lmodvsghm  20878  lssset  20888  lspfval  20928  islbs  21032  sraval  21131  rlmval  21147  2idlval  21210  lpival  21283  expmhm  21402  expghm  21434  mulgghm2  21435  mulgrhm  21436  zrhval  21466  zrhmulg  21468  zlmval  21474  chrval  21482  znval  21494  znzrhval  21505  evpmss  21544  psgnevpmb  21545  ip0l  21594  ipffval  21606  ocvfval  21624  ocvval  21625  cssval  21640  thlval  21653  pjfval  21664  pjval  21668  isobs  21678  prdsinvgd2  21700  uvcresum  21751  frlmup1  21756  frlmup2  21757  islinds  21767  islindf5  21797  aspval  21831  asclval  21838  psrmulval  21902  psrlidm  21920  psrridm  21921  psrascl  21937  mvrval  21940  mvrval2  21941  mplmonmul  21992  evlslem3  22036  evlslem1  22038  evlsval  22042  evlssca  22045  evlsvar  22046  psdmul  22102  psdmvr  22105  psr1val  22119  vr1val  22125  ply1val  22127  coe1fval  22139  coe1fv  22140  coe1tmmul2  22211  coe1tmmul  22212  coe1tmmul2fv  22213  coe1pwmulfv  22215  evls1val  22256  evl1fval  22264  evl1val  22265  mamulid  22377  mamurid  22378  mdetleib  22523  mdetleib1  22527  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  cpmidpmatlem1  22806  ordtval  23125  cnpval  23172  ptpjpre1  23507  ptpjopn  23548  dfac14  23554  upxp  23559  uptx  23561  hauseqlcld  23582  txlm  23584  xkoptsub  23590  xkoinjcn  23623  kqval  23662  xpstopnlem1  23745  fmval  23879  flfval  23926  ptcmplem2  23989  ptcmplem3  23990  symgtgp  24042  qustgpopn  24056  ussval  24196  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  mopnval  24375  prdsxmslem2  24466  nmfval  24525  nmval  24526  nmoval  24652  metdsval  24785  divcnOLD  24806  divcn  24808  mulc1cncf  24847  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  cnheiborlem  24902  evth  24907  evth2  24908  lebnumlem3  24911  isphtpy  24929  isphtpc  24942  pcofval  24959  pcovalg  24961  pco1  24964  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevcl  24974  pcorevlem  24975  pcorev2  24977  pi1xfrcnv  25006  cphnm  25143  tcphval  25168  tcphnmval  25179  cfilfval  25214  iscmet  25234  iscmet3lem3  25240  rrxval  25337  ehlval  25364  ivth2  25406  ovolval  25424  ovollb2lem  25439  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliunlem2  25454  ovolicc1  25467  voliunlem1  25501  voliunlem2  25502  voliunlem3  25503  volsup  25507  ioorval  25525  uniioombllem3  25536  uniioombllem6  25539  volsup2  25556  volcn  25557  volivth  25558  vitalilem2  25560  vitalilem3  25561  vitalilem4  25562  vitali  25564  mbfmax  25600  mbfimaopnlem  25606  itg1val  25634  i1f1lem  25640  itg11  25642  itg1addlem4  25650  itg1mulc  25655  i1fres  25656  itg1climres  25665  mbfi1fseqlem2  25667  mbfi1fseqlem3  25668  mbfi1fseqlem6  25671  mbfi1flimlem  25673  mbfi1flim  25674  mbfmullem2  25675  itg2seq  25693  itg2uba  25694  itg2splitlem  25699  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  itg2cnlem1  25712  itg2cn  25714  limccnp2  25843  dvnff  25875  dvnp1  25877  cpnfval  25884  elcpn  25886  dvrec  25909  dvcnvlem  25930  dveflem  25933  dvef  25934  dvferm1  25939  dvferm2  25941  rolle  25944  dvlip  25948  dvlipcn  25949  dv11cn  25956  dvivthlem1  25963  dvivth  25965  lhop1lem  25968  ftc1lem1  25992  ftc1lem5  25997  ftc2  26001  itgsubstlem  26005  tdeglem3  26014  tdeglem4  26015  mdegval  26018  mdegmullem  26033  deg1fval  26035  deg1ldg  26047  deg1leb  26050  coe1mul3  26054  uc1pval  26095  mon1pval  26097  mon1pid  26109  q1pval  26110  r1pval  26113  ply1remlem  26120  ig1pval  26131  plyval  26148  elply2  26151  plyeq0lem  26165  coeval  26178  dgrval  26183  coeid2  26194  coemullem  26205  coemul  26207  elqaalem1  26277  elqaalem2  26278  elqaalem3  26279  iaa  26283  aareccl  26284  aannenlem1  26286  geolim3  26297  aaliou3lem1  26300  aaliou3lem2  26301  aaliou3lem5  26305  aaliou3lem6  26306  aaliou3lem7  26307  aaliou3  26309  tayl0  26319  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmshftlem  26348  ulmshft  26349  ulmuni  26351  ulmcau  26354  ulmdvlem1  26359  ulmdvlem3  26361  mtest  26363  mtestbdd  26364  mbfulm  26365  iblulm  26366  itgulm  26367  pserval  26369  pserval2  26370  radcnvlem1  26372  radcnvlem2  26373  dvradcnv  26380  pserulm  26381  pserdvlem2  26388  pserdv  26389  abelthlem1  26391  abelthlem3  26393  abelthlem4  26394  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem8  26399  abelthlem9  26400  resinf1o  26495  efif1olem4  26504  eff1olem  26507  logcnlem5  26605  logtayllem  26618  logtayl  26619  logtaylsum  26620  logtayl2  26621  logccv  26622  asinval  26842  acosval  26843  atanval  26844  atantayl  26897  leibpilem2  26901  leibpi  26902  leibpisum  26903  log2cnv  26904  log2tlbnd  26905  areaval  26924  efrlim  26929  efrlimOLD  26930  dfef2  26931  amgmlem  26950  emcllem2  26957  emcllem3  26958  emcllem4  26959  emcllem5  26960  emcllem6  26961  emcllem7  26962  zetacvg  26975  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulm2  26996  lgamcvglem  27000  igamval  27007  lgamcvg2  27015  gamcvg2lem  27019  ftalem7  27039  basellem2  27042  basellem3  27043  basellem4  27044  basellem5  27045  basellem6  27046  basellem8  27048  basellem9  27049  chtval  27070  vmaval  27073  chpval  27082  ppival  27087  muval  27092  prmorcht  27138  sqff1o  27142  dvdsflsumcom  27148  musum  27151  muinv  27153  sgmppw  27158  fsumvma  27174  pclogsum  27176  dchrfi  27216  bposlem5  27249  bposlem7  27251  bposlem8  27252  bposlem9  27253  lgsfval  27263  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  lgsqrlem2  27308  lgsqrlem4  27310  lgseisenlem2  27337  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasumiflem1  27462  dchrvmaeq0  27465  dchrisum0fval  27466  dchrisum0re  27474  mulog2sumlem1  27495  pntrval  27523  pntsval  27533  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntlem3  27570  abvcxp  27576  padicfval  27577  padicval  27578  padicabv  27591  ostth1  27594  ostth2  27598  ostth3  27599  nosupfv  27668  noinffv  27683  newval  27811  leftval  27819  rightval  27820  iscgrg  28437  legval  28509  ishpg  28684  iscgra  28734  isinag  28763  isleag  28772  iseqlg  28792  ttgval  28800  elee  28819  axsegconlem1  28842  axsegconlem9  28850  axsegconlem10  28851  axpasch  28866  axlowdimlem15  28881  axlowdim  28886  axeuclidlem  28887  axcontlem2  28890  eengv  28904  vtxval  28925  iedgval  28926  edgval  28974  vtxdgval  29394  wwlksnextinj  29827  wwlksnextsurj  29828  clwwlkfv  29975  clwwlknonmpo  30016  fusgreg2wsplem  30260  fusgreghash2wsp  30265  numclwwlk1lem2fv  30283  gidval  30439  grpoinvval  30450  bafval  30531  imsval  30612  dipfval  30629  sspval  30650  nmooval  30690  hmoval  30737  ipasslem8  30764  ipasslem9  30765  ipblnfi  30782  ubthlem2  30798  htthlem  30844  normval  31051  ocval  31207  occllem  31230  hsupval  31261  pjhfval  31323  pjhval  31324  chscllem2  31565  chscllem3  31566  hosval  31667  homval  31668  hodval  31669  hfsval  31670  hfmval  31671  brafval  31870  braval  31871  kbval  31881  eigvalval  31887  cnlnadjlem1  31994  nmopadjlei  32015  hmopidmchi  32078  strlem2  32178  hstrlem2  32186  cdj3lem2  32362  ofpreima  32589  psgnfzto1stlem  33057  evpmval  33102  altgnsg  33106  inftmrel  33124  isinftm  33125  qusker  33310  qusvscpbl  33312  qusvsval  33313  mxidlval  33422  idlsrgval  33464  dimval  33586  dimvalfi  33587  smatfval  33772  lmatval  33790  locfinreflem  33817  rspecval  33841  rmulccn  33905  xrmulc1cn  33907  xrge0iifcv  33911  xrge0iifiso  33912  xrge0iifhom  33914  xrge0iif1  33915  qqhval  33949  rrhval  33973  xrhval  33995  ddeval1  34211  ddeval0  34212  sxbrsigalem0  34249  sxbrsigalem3  34250  eulerpartlemgv  34351  rrvmbfm  34420  dstrvval  34449  coinflippv  34462  ballotlem2  34467  ballotlemfval  34468  ballotlemi  34479  ballotlemsval  34487  ballotlemrval  34496  ballotth  34516  plymulx  34526  signstfv  34541  signsvvfval  34556  derangval  35135  subfacval  35141  erdszelem3  35161  erdszelem9  35167  erdszelem10  35168  txpconn  35200  indispconn  35202  cvxpconn  35210  cvmlift2lem2  35272  cvmlift2lem3  35273  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmlift3lem4  35290  snmlfval  35298  snmlval  35299  gonafv  35318  mvtval  35468  mrsubffval  35475  mrsubcv  35478  mrsubrn  35481  elmrsubrn  35488  msubffval  35491  mvhval  35502  mpstval  35503  mstaval  35512  mclsval  35531  mppsval  35540  sinccvglem  35640  circum  35642  divcnvlin  35696  iprodefisum  35704  iprodgam  35705  faclimlem1  35706  faclimlem2  35707  faclim  35709  iprodfac  35710  faclim2  35711  dfrdg2  35759  findabrcl  36418  dnival  36435  bj-evalval  37039  bj-inftyexpitaudisj  37169  bj-inftyexpiinv  37172  bj-inftyexpidisj  37174  curfv  37570  finixpnum  37575  poimirlem16  37606  poimir  37623  broucube  37624  mblfinlem2  37628  voliunnfl  37634  volsupnfl  37635  itg2addnclem  37641  itg2addnclem3  37643  ftc1cnnc  37662  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anc  37671  ftc2nc  37672  fvopabf4g  37692  sdclem2  37712  fdc  37715  lmclim2  37728  geomcau  37729  istotbnd  37739  isbnd  37750  prdsbnd2  37765  heiborlem6  37786  heiborlem7  37787  heiborlem8  37788  rrnval  37797  rrncmslem  37802  idlval  37983  pridlval  38003  maxidlval  38009  lshpset  38942  lsatset  38954  lcvfbr  38984  lflset  39023  lflnegcl  39039  lshpkrlem1  39074  lshpkrlem2  39075  lshpkrlem3  39076  ldualset  39089  cmtfvalN  39174  cvrfval  39232  pats  39249  llnset  39470  lplnset  39494  lvolset  39537  lineset  39703  pointsetN  39706  psubspset  39709  pmapval  39722  paddfval  39762  pclfvalN  39854  polfvalN  39869  polvalN  39870  psubclsetN  39901  watvalN  39958  lhpset  39960  lautset  40047  pautsetN  40063  ldilset  40074  ltrnset  40083  dilsetN  40118  trnsetN  40121  trlset  40126  trlval  40127  tgrpset  40710  tendoset  40724  tendo02  40752  erngset  40765  erngset-rN  40773  cdlemksv  40809  dvaset  40970  dvaplusgv  40975  diafval  40996  diaval  40997  dvhset  41046  cdlemm10N  41083  docafvalN  41087  djafvalN  41099  dibfval  41106  dibval  41107  dicfval  41140  dicval  41141  dihval  41197  dochfval  41315  djhfval  41362  dochfl1  41441  lpolsetN  41447  lcdval  41554  mapdhval  41689  hvmapfval  41724  hdmap1fval  41761  fimgmcyc  42504  prjspval  42573  isnacs  42674  mzpclval  42695  mzpsubst  42718  mzprename  42719  mzpcompact2lem  42721  eldiophb  42727  diophrw  42729  eldioph2  42732  diophin  42742  diophun  42743  diophren  42783  pell1qrval  42816  pell14qrval  42818  pell1234qrval  42820  pellfundval  42850  rmxypairf1o  42882  rmxyval  42886  mzpcong  42943  pw2f1ocnv  43008  dnnumch1  43015  dfac11  43033  hbtlem1  43094  hbtlem7  43096  elmnc  43107  dgraaval  43115  mpaaval  43122  itgoval  43132  flcidc  43141  mendval  43150  cytpval  43173  cantnfub  43292  cantnfresb  43295  tfsconcatrev  43319  elcnvlem  43572  comptiunov2i  43677  dftrcl3  43691  trclfvcom  43694  cnvtrclfv  43695  cotrcltrcl  43696  trclimalb2  43697  trclfvdecomr  43699  dfrtrcl3  43704  dfrtrcl4  43709  clsk1indlem0  44012  clsk1indlem2  44013  clsk1indlem3  44014  clsk1indlem4  44015  clsk1indlem1  44016  k0004val  44121  lhe4.4ex1a  44301  addrfv  44441  subrfv  44442  mulvfv  44443  monoord2xrv  45458  sumnnodd  45607  liminfgval  45739  ioodvbdlimc2lem  45911  itgsin0pilem1  45927  stoweidlem55  46032  wallispilem1  46042  wallispilem2  46043  wallispilem4  46045  wallispi2lem1  46048  wallispi2lem2  46049  dirkerval  46068  fourierdlem2  46086  fourierdlem3  46087  fourierdlem29  46113  fourierdlem62  46145  fourierdlem80  46163  fourierdlem103  46186  fourierdlem104  46187  fourierswlem  46207  fouriersw  46208  iundjiunlem  46436  carageniuncllem2  46499  0ome  46506  hoidmv1le  46571  hoidmvlelem3  46574  smflimsuplem7  46803  iccpval  47377  fppr  47688  bigoval  48477  ackval0  48608  ackval41a  48622  eenglngeehlnm  48667  oppcinito  49100  oppctermo  49101  dfinito4  49334  prstcval  49376  mndtcval  49404  setc1onsubc  49427  lmdfval2  49475  cmdfval2  49476  vsetrec  49515  onsetreclem1  49517  elpglem3  49525  pgindnf  49528  sinhval-named  49548  coshval-named  49549  tanhval-named  49550  secval  49559  cscval  49560  cotval  49561  aacllem  49613