Theorem fvmpt 6935

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3437   ↦ cmpt 5174  ‘cfv 6486

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmptex  6949  fvmptrabfv  6967  mptfvmpt  7168  fvmptopab  7407  ofval  7627  caofinvl  7648  fvresex  7898  1stval  7929  2ndval  7930  reldm  7982  curry1val  8041  curry2val  8045  fsplitfpar  8054  fnwelem  8067  brtpos2  8168  onovuni  8268  tz7.44-1  8331  oasuc  8445  oesuclem  8446  omsuc  8447  onasuc  8449  onmsuc  8450  fsetfocdm  8791  fvmptmap  8811  xpcomco  8987  unxpdomlem1  9147  unfilem2  9197  ordtypelem3  9413  ixpiunwdom  9483  inf3lema  9521  noinfep  9557  cantnfval  9565  cantnflem1d  9585  cantnflem1  9586  ssttrcl  9612  ttrcltr  9613  ttrclselem2  9623  r1sucg  9669  r0weon  9910  infxpenc2lem1  9917  fseqenlem1  9922  fseqenlem2  9923  dfac8alem  9927  ac5num  9934  acni2  9944  dfac4  10020  dfac2a  10028  dfacacn  10040  dfac12lem1  10042  ackbij1lem7  10123  ackbij2lem2  10137  ackbij2lem3  10138  cfsmolem  10168  fin23lem28  10238  fin23lem39  10248  isf32lem6  10256  isf32lem7  10257  isf32lem8  10258  fin1a2lem3  10300  itunifval  10314  itunisuc  10317  axdc2lem  10346  axdc3lem2  10349  axcclem  10355  zorn2lem1  10394  negiso  12109  infrenegsup  12112  uzval  12740  flval  13700  ceilval  13744  ceilval2  13746  monoord2  13942  seqf1olem2  13951  seqf1o  13952  seqdistr  13962  serle  13966  seqof  13968  swrdfv  14558  revval  14669  revfv  14672  wwlktovf1  14866  wwlktovfo  14867  sgnval  14997  cjval  15011  reval  15015  imval  15016  sqrtval  15146  absval  15147  limsupval  15383  limsupgval  15385  climmpt  15480  climle  15549  rlimdiv  15555  isercolllem1  15574  isercoll2  15578  caurcvg2  15587  fsumser  15639  isumadd  15676  fsumcnv  15682  fsumrev  15688  fsumshft  15689  iserabs  15724  cvgcmp  15725  cvgcmpce  15727  incexclem  15745  isumless  15754  divcnvshft  15764  supcvg  15765  harmonic  15768  trireciplem  15771  trirecip  15772  expcnv  15773  explecnv  15774  geolim  15779  geolim2  15780  geo2lim  15784  geomulcvg  15785  geoisum  15786  geoisumr  15787  geoisum1  15788  geoisum1c  15789  cvgrat  15792  mertenslem2  15794  mertens  15795  prodfdiv  15805  fprodser  15858  fprodshft  15885  fprodrev  15886  fprodcnv  15892  iprodmul  15912  bpolylem  15957  eftval  15985  efval  15988  efcvgfsum  15995  ege2le3  15999  eftlub  16020  eflegeo  16032  sinval  16033  cosval  16034  tanval  16039  eirrlem  16115  rpnnen2lem1  16125  rpnnen2lem2  16126  bitsfval  16336  bitsinv2  16356  bitsinv  16361  sadcf  16366  sadc0  16367  sadcp1  16368  smupf  16391  smup0  16392  smupp1  16393  qnumval  16650  qdenval  16651  phival  16680  crth  16691  phimullem  16692  eulerthlem2  16695  phisum  16704  odzval  16705  iserodd  16749  pcmpt  16806  prmreclem1  16830  prmreclem2  16831  prmreclem4  16833  prmreclem5  16834  prmreclem6  16835  1arithlem1  16837  1arithlem2  16838  vdwapfval  16885  vdwlem2  16896  vdwlem6  16900  vdwlem8  16902  vdwlem9  16903  ramub1lem2  16941  ramcl  16943  prmoval  16947  strfvnd  17098  topnval  17340  prdsplusgfval  17380  prdsmulrfval  17382  isacs  17559  acsfn  17567  homffval  17598  comfffval  17606  oppcval  17621  monfval  17641  oppcmon  17647  sectffval  17659  invffval  17667  isoval  17674  idfuval  17785  homafval  17938  arwval  17952  coafval  17973  yonedainv  18189  oduval  18196  pltfval  18237  lubfval  18256  lubval  18262  glbfval  18269  glbval  18275  p0val  18333  p1val  18334  ipoval  18438  plusffval  18556  grpidval  18571  issubmgm  18612  issubm  18713  prdspjmhm  18739  efmnd  18780  smndex1igid  18814  grpinvfval  18893  grpinvval  18895  grpsubfval  18898  grpsubfvalALT  18899  grplactval  18957  prdsinvlem  18964  mulgfval  18984  mulgfvalALT  18985  pwsmulg  19034  issubg  19041  isnsg  19069  cycsubmel  19114  cycsubgcl  19120  conjghm  19163  conjnmz  19166  cntrval  19233  cntzfval  19234  cntzval  19235  oppgval  19261  psgnfval  19414  psgnval  19421  odfval  19446  odval  19448  sylow1lem4  19515  pgpssslw  19528  sylow2blem3  19536  sylow3lem2  19542  lsmfval  19552  pj1fval  19608  efgval  19631  efgsval  19645  frgpval  19672  vrgpval  19681  mulgmhm  19741  mulgghm  19742  ablfaclem1  20001  mgpval  20063  srglmhm  20141  srgrmhm  20142  ringlghm  20232  ringrghm  20233  pwspjmhmmgpd  20248  pwsexpg  20249  opprval  20258  dvdsrval  20281  isunit  20293  invrfval  20309  dvrfval  20322  isirred  20339  issubrng  20464  issubrg  20488  rgspnval  20529  rrgval  20614  fidomndrnglem  20689  issdrg  20705  abvfval  20727  abvtrivd  20749  staffval  20758  stafval  20759  scaffval  20815  lmodvsghm  20858  lssset  20868  lspfval  20908  islbs  21012  sraval  21111  rlmval  21127  2idlval  21190  lpival  21263  expmhm  21375  expghm  21414  mulgghm2  21415  mulgrhm  21416  zrhval  21446  zrhmulg  21448  zlmval  21454  chrval  21462  znval  21474  znzrhval  21485  evpmss  21525  psgnevpmb  21526  ip0l  21575  ipffval  21587  ocvfval  21605  ocvval  21606  cssval  21621  thlval  21634  pjfval  21645  pjval  21649  isobs  21659  prdsinvgd2  21681  uvcresum  21732  frlmup1  21737  frlmup2  21738  islinds  21748  islindf5  21778  aspval  21812  asclval  21819  psrmulval  21883  psrlidm  21900  psrridm  21901  psrascl  21917  mvrval  21920  mvrval2  21921  mplmonmul  21972  evlslem3  22016  evlslem1  22018  evlsval  22022  evlssca  22025  evlsvar  22026  psdmul  22082  psdmvr  22085  psr1val  22099  vr1val  22105  ply1val  22107  coe1fval  22119  coe1fv  22120  coe1tmmul2  22191  coe1tmmul  22192  coe1tmmul2fv  22193  coe1pwmulfv  22195  evls1val  22236  evl1fval  22244  evl1val  22245  mamulid  22357  mamurid  22358  mdetleib  22503  mdetleib1  22507  mdetunilem9  22536  mdetuni0  22537  mdetmul  22539  cpmidpmatlem1  22786  ordtval  23105  cnpval  23152  ptpjpre1  23487  ptpjopn  23528  dfac14  23534  upxp  23539  uptx  23541  hauseqlcld  23562  txlm  23564  xkoptsub  23570  xkoinjcn  23603  kqval  23642  xpstopnlem1  23725  fmval  23859  flfval  23906  ptcmplem2  23969  ptcmplem3  23970  symgtgp  24022  qustgpopn  24036  ussval  24175  iscfilu  24203  ispsmet  24220  ismet  24239  isxmet  24240  mopnval  24354  prdsxmslem2  24445  nmfval  24504  nmval  24505  nmoval  24631  metdsval  24764  divcnOLD  24785  divcn  24787  mulc1cncf  24826  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  cnheiborlem  24881  evth  24886  evth2  24887  lebnumlem3  24890  isphtpy  24908  isphtpc  24921  pcofval  24938  pcovalg  24940  pco1  24943  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevcl  24953  pcorevlem  24954  pcorev2  24956  pi1xfrcnv  24985  cphnm  25121  tcphval  25146  tcphnmval  25157  cfilfval  25192  iscmet  25212  iscmet3lem3  25218  rrxval  25315  ehlval  25342  ivth2  25384  ovolval  25402  ovollb2lem  25417  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliunlem2  25432  ovolicc1  25445  voliunlem1  25479  voliunlem2  25480  voliunlem3  25481  volsup  25485  ioorval  25503  uniioombllem3  25514  uniioombllem6  25517  volsup2  25534  volcn  25535  volivth  25536  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  vitali  25542  mbfmax  25578  mbfimaopnlem  25584  itg1val  25612  i1f1lem  25618  itg11  25620  itg1addlem4  25628  itg1mulc  25633  i1fres  25634  itg1climres  25643  mbfi1fseqlem2  25645  mbfi1fseqlem3  25646  mbfi1fseqlem6  25649  mbfi1flimlem  25651  mbfi1flim  25652  mbfmullem2  25653  itg2seq  25671  itg2uba  25672  itg2splitlem  25677  itg2monolem1  25679  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2i1fseqle  25683  itg2i1fseq  25684  itg2i1fseq2  25685  itg2addlem  25687  itg2cnlem1  25690  itg2cn  25692  limccnp2  25821  dvnff  25853  dvnp1  25855  cpnfval  25862  elcpn  25864  dvrec  25887  dvcnvlem  25908  dveflem  25911  dvef  25912  dvferm1  25917  dvferm2  25919  rolle  25922  dvlip  25926  dvlipcn  25927  dv11cn  25934  dvivthlem1  25941  dvivth  25943  lhop1lem  25946  ftc1lem1  25970  ftc1lem5  25975  ftc2  25979  itgsubstlem  25983  tdeglem3  25992  tdeglem4  25993  mdegval  25996  mdegmullem  26011  deg1fval  26013  deg1ldg  26025  deg1leb  26028  coe1mul3  26032  uc1pval  26073  mon1pval  26075  mon1pid  26087  q1pval  26088  r1pval  26091  ply1remlem  26098  ig1pval  26109  plyval  26126  elply2  26129  plyeq0lem  26143  coeval  26156  dgrval  26161  coeid2  26172  coemullem  26183  coemul  26185  elqaalem1  26255  elqaalem2  26256  elqaalem3  26257  iaa  26261  aareccl  26262  aannenlem1  26264  geolim3  26275  aaliou3lem1  26278  aaliou3lem2  26279  aaliou3lem5  26283  aaliou3lem6  26284  aaliou3lem7  26285  aaliou3  26287  tayl0  26297  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmshftlem  26326  ulmshft  26327  ulmuni  26329  ulmcau  26332  ulmdvlem1  26337  ulmdvlem3  26339  mtest  26341  mtestbdd  26342  mbfulm  26343  iblulm  26344  itgulm  26345  pserval  26347  pserval2  26348  radcnvlem1  26350  radcnvlem2  26351  dvradcnv  26358  pserulm  26359  pserdvlem2  26366  pserdv  26367  abelthlem1  26369  abelthlem3  26371  abelthlem4  26372  abelthlem5  26373  abelthlem6  26374  abelthlem7  26376  abelthlem8  26377  abelthlem9  26378  resinf1o  26473  efif1olem4  26482  eff1olem  26485  logcnlem5  26583  logtayllem  26596  logtayl  26597  logtaylsum  26598  logtayl2  26599  logccv  26600  asinval  26820  acosval  26821  atanval  26822  atantayl  26875  leibpilem2  26879  leibpi  26880  leibpisum  26881  log2cnv  26882  log2tlbnd  26883  areaval  26902  efrlim  26907  efrlimOLD  26908  dfef2  26909  amgmlem  26928  emcllem2  26935  emcllem3  26936  emcllem4  26937  emcllem5  26938  emcllem6  26939  emcllem7  26940  zetacvg  26953  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulm2  26974  lgamcvglem  26978  igamval  26985  lgamcvg2  26993  gamcvg2lem  26997  ftalem7  27017  basellem2  27020  basellem3  27021  basellem4  27022  basellem5  27023  basellem6  27024  basellem8  27026  basellem9  27027  chtval  27048  vmaval  27051  chpval  27060  ppival  27065  muval  27070  prmorcht  27116  sqff1o  27120  dvdsflsumcom  27126  musum  27129  muinv  27131  sgmppw  27136  fsumvma  27152  pclogsum  27154  dchrfi  27194  bposlem5  27227  bposlem7  27229  bposlem8  27230  bposlem9  27231  lgsfval  27241  lgsdir  27271  lgsdilem2  27272  lgsdi  27273  lgsne0  27274  lgsqrlem2  27286  lgsqrlem4  27288  lgseisenlem2  27315  dchrmusum2  27433  dchrvmasumlem1  27434  dchrvmasumiflem1  27440  dchrvmaeq0  27443  dchrisum0fval  27444  dchrisum0re  27452  mulog2sumlem1  27473  pntrval  27501  pntsval  27511  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntlem3  27548  abvcxp  27554  padicfval  27555  padicval  27556  padicabv  27569  ostth1  27572  ostth2  27576  ostth3  27577  nosupfv  27646  noinffv  27661  newval  27797  leftval  27805  rightval  27806  iscgrg  28491  legval  28563  ishpg  28738  iscgra  28788  isinag  28817  isleag  28826  iseqlg  28846  ttgval  28854  elee  28873  axsegconlem1  28897  axsegconlem9  28905  axsegconlem10  28906  axpasch  28921  axlowdimlem15  28936  axlowdim  28941  axeuclidlem  28942  axcontlem2  28945  eengv  28959  vtxval  28980  iedgval  28981  edgval  29029  vtxdgval  29449  wwlksnextinj  29879  wwlksnextsurj  29880  clwwlkfv  30030  clwwlknonmpo  30071  fusgreg2wsplem  30315  fusgreghash2wsp  30320  numclwwlk1lem2fv  30338  gidval  30494  grpoinvval  30505  bafval  30586  imsval  30667  dipfval  30684  sspval  30705  nmooval  30745  hmoval  30792  ipasslem8  30819  ipasslem9  30820  ipblnfi  30837  ubthlem2  30853  htthlem  30899  normval  31106  ocval  31262  occllem  31285  hsupval  31316  pjhfval  31378  pjhval  31379  chscllem2  31620  chscllem3  31621  hosval  31722  homval  31723  hodval  31724  hfsval  31725  hfmval  31726  brafval  31925  braval  31926  kbval  31936  eigvalval  31942  cnlnadjlem1  32049  nmopadjlei  32070  hmopidmchi  32133  strlem2  32233  hstrlem2  32241  cdj3lem2  32417  ofpreima  32649  psgnfzto1stlem  33076  evpmval  33121  altgnsg  33125  inftmrel  33156  isinftm  33157  qusker  33321  qusvscpbl  33323  qusvsval  33324  mxidlval  33433  idlsrgval  33475  dimval  33634  dimvalfi  33635  smatfval  33829  lmatval  33847  locfinreflem  33874  rspecval  33898  rmulccn  33962  xrmulc1cn  33964  xrge0iifcv  33968  xrge0iifiso  33969  xrge0iifhom  33971  xrge0iif1  33972  qqhval  34006  rrhval  34030  xrhval  34052  ddeval1  34268  ddeval0  34269  sxbrsigalem0  34305  sxbrsigalem3  34306  eulerpartlemgv  34407  rrvmbfm  34476  dstrvval  34505  coinflippv  34518  ballotlem2  34523  ballotlemfval  34524  ballotlemi  34535  ballotlemsval  34543  ballotlemrval  34552  ballotth  34572  plymulx  34582  signstfv  34597  signsvvfval  34612  onvf1odlem3  35170  derangval  35232  subfacval  35238  erdszelem3  35258  erdszelem9  35264  erdszelem10  35265  txpconn  35297  indispconn  35299  cvxpconn  35307  cvmlift2lem2  35369  cvmlift2lem3  35370  cvmlift2lem7  35374  cvmliftphtlem  35382  cvmlift3lem4  35387  snmlfval  35395  snmlval  35396  gonafv  35415  mvtval  35565  mrsubffval  35572  mrsubcv  35575  mrsubrn  35578  elmrsubrn  35585  msubffval  35588  mvhval  35599  mpstval  35600  mstaval  35609  mclsval  35628  mppsval  35637  sinccvglem  35737  circum  35739  divcnvlin  35798  iprodefisum  35806  iprodgam  35807  faclimlem1  35808  faclimlem2  35809  faclim  35811  iprodfac  35812  faclim2  35813  dfrdg2  35858  findabrcl  36519  dnival  36536  bj-evalval  37140  bj-inftyexpitaudisj  37270  bj-inftyexpiinv  37273  bj-inftyexpidisj  37275  curfv  37660  finixpnum  37665  poimirlem16  37696  poimir  37713  broucube  37714  mblfinlem2  37718  voliunnfl  37724  volsupnfl  37725  itg2addnclem  37731  itg2addnclem3  37733  ftc1cnnc  37752  ftc1anclem5  37757  ftc1anclem6  37758  ftc1anclem7  37759  ftc1anc  37761  ftc2nc  37762  fvopabf4g  37782  sdclem2  37802  fdc  37805  lmclim2  37818  geomcau  37819  istotbnd  37829  isbnd  37840  prdsbnd2  37855  heiborlem6  37876  heiborlem7  37877  heiborlem8  37878  rrnval  37887  rrncmslem  37892  idlval  38073  pridlval  38093  maxidlval  38099  lshpset  39097  lsatset  39109  lcvfbr  39139  lflset  39178  lflnegcl  39194  lshpkrlem1  39229  lshpkrlem2  39230  lshpkrlem3  39231  ldualset  39244  cmtfvalN  39329  cvrfval  39387  pats  39404  llnset  39624  lplnset  39648  lvolset  39691  lineset  39857  pointsetN  39860  psubspset  39863  pmapval  39876  paddfval  39916  pclfvalN  40008  polfvalN  40023  polvalN  40024  psubclsetN  40055  watvalN  40112  lhpset  40114  lautset  40201  pautsetN  40217  ldilset  40228  ltrnset  40237  dilsetN  40272  trnsetN  40275  trlset  40280  trlval  40281  tgrpset  40864  tendoset  40878  tendo02  40906  erngset  40919  erngset-rN  40927  cdlemksv  40963  dvaset  41124  dvaplusgv  41129  diafval  41150  diaval  41151  dvhset  41200  cdlemm10N  41237  docafvalN  41241  djafvalN  41253  dibfval  41260  dibval  41261  dicfval  41294  dicval  41295  dihval  41351  dochfval  41469  djhfval  41516  dochfl1  41595  lpolsetN  41601  lcdval  41708  mapdhval  41843  hvmapfval  41878  hdmap1fval  41915  fimgmcyc  42652  prjspval  42721  isnacs  42821  mzpclval  42842  mzpsubst  42865  mzprename  42866  mzpcompact2lem  42868  eldiophb  42874  diophrw  42876  eldioph2  42879  diophin  42889  diophun  42890  diophren  42930  pell1qrval  42963  pell14qrval  42965  pell1234qrval  42967  pellfundval  42997  rmxypairf1o  43028  rmxyval  43032  mzpcong  43089  pw2f1ocnv  43154  dnnumch1  43161  dfac11  43179  hbtlem1  43240  hbtlem7  43242  elmnc  43253  dgraaval  43261  mpaaval  43268  itgoval  43278  flcidc  43287  mendval  43296  cytpval  43319  cantnfub  43438  cantnfresb  43441  tfsconcatrev  43465  elcnvlem  43718  comptiunov2i  43823  dftrcl3  43837  trclfvcom  43840  cnvtrclfv  43841  cotrcltrcl  43842  trclimalb2  43843  trclfvdecomr  43845  dfrtrcl3  43850  dfrtrcl4  43855  clsk1indlem0  44158  clsk1indlem2  44159  clsk1indlem3  44160  clsk1indlem4  44161  clsk1indlem1  44162  k0004val  44267  lhe4.4ex1a  44446  addrfv  44585  subrfv  44586  mulvfv  44587  monoord2xrv  45605  sumnnodd  45754  liminfgval  45884  ioodvbdlimc2lem  46056  itgsin0pilem1  46072  stoweidlem55  46177  wallispilem1  46187  wallispilem2  46188  wallispilem4  46190  wallispi2lem1  46193  wallispi2lem2  46194  dirkerval  46213  fourierdlem2  46231  fourierdlem3  46232  fourierdlem29  46258  fourierdlem62  46290  fourierdlem80  46308  fourierdlem103  46331  fourierdlem104  46332  fourierswlem  46352  fouriersw  46353  iundjiunlem  46581  carageniuncllem2  46644  0ome  46651  hoidmv1le  46716  hoidmvlelem3  46719  smflimsuplem7  46948  nthrucw  47008  iccpval  47539  fppr  47850  bigoval  48674  ackval0  48805  ackval41a  48819  eenglngeehlnm  48864  oppcinito  49360  oppctermo  49361  dfinito4  49626  prstcval  49676  mndtcval  49704  setc1onsubc  49727  lmdfval2  49780  cmdfval2  49781  vsetrec  49828  onsetreclem1  49830  elpglem3  49838  pgindnf  49841  sinhval-named  49861  coshval-named  49862  tanhval-named  49863  secval  49872  cscval  49873  cotval  49874  aacllem  49926