Theorem fvmpt 6970

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ↦ cmpt 5178  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6472  df-fun 6518  df-fv 6524

This theorem is referenced by:  fvmptex  6985  fvmptrabfv  7003  mptfvmpt  7207  fvmptopab  7446  ofval  7666  caofinvl  7687  fvresex  7936  1stval  7967  2ndval  7968  reldm  8020  curry1val  8078  curry2val  8082  fsplitfpar  8091  fnwelem  8105  brtpos2  8206  onovuni  8307  tz7.44-1  8371  oasuc  8487  oesuclem  8488  omsuc  8489  onasuc  8491  onmsuc  8492  fsetfocdm  8836  fvmptmap  8857  xpcomco  9033  unxpdomlem1  9194  unfilem2  9244  ordtypelem3  9462  ixpiunwdom  9532  inf3lema  9573  noinfep  9609  cantnfval  9617  cantnflem1d  9637  cantnflem1  9638  ssttrcl  9664  ttrcltr  9665  ttrclselem2  9675  r1sucg  9721  r0weon  9962  infxpenc2lem1  9969  fseqenlem1  9974  fseqenlem2  9975  dfac8alem  9979  ac5num  9986  acni2  9996  dfac4  10072  dfac2a  10080  dfacacn  10092  dfac12lem1  10094  ackbij1lem7  10175  ackbij2lem2  10189  ackbij2lem3  10190  cfsmolem  10221  fin23lem28  10291  fin23lem39  10301  isf32lem6  10309  isf32lem7  10310  isf32lem8  10311  fin1a2lem3  10353  itunifval  10367  itunisuc  10370  axdc2lem  10399  axdc3lem2  10402  axcclem  10408  zorn2lem1  10447  negiso  12166  infrenegsup  12169  uzval  12835  flval  13798  ceilval  13842  ceilval2  13844  monoord2  14040  seqf1olem2  14049  seqf1o  14050  seqdistr  14060  serle  14064  seqof  14066  swrdfv  14656  revval  14767  revfv  14770  wwlktovf1  14964  wwlktovfo  14965  sgnval  15095  cjval  15120  reval  15124  imval  15125  sqrtval  15255  absval  15256  limsupval  15492  limsupgval  15494  climmpt  15589  climle  15658  rlimdiv  15664  isercolllem1  15683  isercoll2  15687  caurcvg2  15696  fsumser  15748  isumadd  15785  fsumcnv  15791  fsumrev  15797  fsumshft  15798  iserabs  15834  cvgcmp  15835  cvgcmpce  15837  incexclem  15857  isumless  15866  divcnvshft  15876  supcvg  15877  harmonic  15880  trireciplem  15883  trirecip  15884  expcnv  15885  explecnv  15886  geolim  15891  geolim2  15892  geo2lim  15896  geomulcvg  15897  geoisum  15898  geoisumr  15899  geoisum1  15900  geoisum1c  15901  cvgrat  15904  mertenslem2  15906  mertens  15907  prodfdiv  15917  fprodser  15970  fprodshft  15997  fprodrev  15998  fprodcnv  16004  iprodmul  16024  bpolylem  16069  eftval  16097  efval  16100  efcvgfsum  16107  ege2le3  16111  eftlub  16132  eflegeo  16144  sinval  16145  cosval  16146  tanval  16151  eirrlem  16227  rpnnen2lem1  16237  rpnnen2lem2  16238  bitsfval  16448  bitsinv2  16468  bitsinv  16473  sadcf  16478  sadc0  16479  sadcp1  16480  smupf  16503  smup0  16504  smupp1  16505  qnumval  16763  qdenval  16764  phival  16793  crth  16804  phimullem  16805  eulerthlem2  16808  phisum  16817  odzval  16818  iserodd  16862  pcmpt  16919  prmreclem1  16943  prmreclem2  16944  prmreclem4  16946  prmreclem5  16947  prmreclem6  16948  1arithlem1  16950  1arithlem2  16951  vdwapfval  16998  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  vdwlem9  17016  ramub1lem2  17054  ramcl  17056  prmoval  17060  strfvnd  17212  topnval  17454  prdsplusgfval  17494  prdsmulrfval  17496  isacs  17674  acsfn  17682  homffval  17713  comfffval  17721  oppcval  17736  monfval  17756  oppcmon  17762  sectffval  17774  invffval  17782  isoval  17789  idfuval  17900  homafval  18053  arwval  18067  coafval  18088  yonedainv  18304  oduval  18311  pltfval  18352  lubfval  18371  lubval  18377  glbfval  18384  glbval  18390  p0val  18448  p1val  18449  ipoval  18553  plusffval  18671  grpidval  18686  issubmgm  18727  issubm  18828  prdspjmhm  18854  efmnd  18895  smndex1gbas  18927  smndex1gid  18929  smndex1igid  18931  smndex1igidOLD  18932  grpinvfval  19011  grpinvval  19013  grpsubfval  19016  grpsubfvalALT  19017  grplactval  19075  prdsinvlem  19082  mulgfval  19102  mulgfvalALT  19103  pwsmulg  19152  issubg  19159  isnsg  19187  cycsubmel  19232  cycsubgcl  19238  conjghm  19280  conjnmz  19283  cntrval  19350  cntzfval  19351  cntzval  19352  oppgval  19378  psgnfval  19531  psgnval  19538  odfval  19563  odval  19565  sylow1lem4  19632  pgpssslw  19645  sylow2blem3  19653  sylow3lem2  19659  lsmfval  19669  pj1fval  19725  efgval  19748  efgsval  19762  frgpval  19789  vrgpval  19798  mulgmhm  19858  mulgghm  19859  ablfaclem1  20118  mgpval  20180  srglmhm  20258  srgrmhm  20259  ringlghm  20349  ringrghm  20350  pwspjmhmmgpd  20363  pwsexpg  20364  opprval  20374  dvdsrval  20397  isunit  20409  invrfval  20425  dvrfval  20438  isirred  20455  issubrng  20584  issubrg  20608  rgspnval  20649  rrgval  20734  fidomndrnglem  20809  issdrg  20825  abvfval  20847  abvtrivd  20869  staffval  20878  stafval  20879  scaffval  20935  lmodvsghm  20978  lssset  20988  lspfval  21028  islbs  21131  sraval  21230  rlmval  21246  2idlval  21309  lpival  21382  expmhm  21476  expghm  21515  mulgghm2  21516  mulgrhm  21517  zrhval  21547  zrhmulg  21549  zlmval  21555  chrval  21563  znval  21575  znzrhval  21586  evpmss  21626  psgnevpmb  21627  ip0l  21676  ipffval  21688  ocvfval  21706  ocvval  21707  cssval  21722  thlval  21735  pjfval  21746  pjval  21750  isobs  21760  prdsinvgd2  21782  uvcresum  21833  frlmup1  21838  frlmup2  21839  islinds  21849  islindf5  21879  aspval  21912  asclval  21919  psrmulval  21984  psrlidm  22001  psrridm  22002  psrascl  22018  mvrval  22021  mvrval2  22022  mplmonmul  22077  evlslem3  22121  evlslem1  22123  evlsval  22127  evlssca  22135  evlsvar  22136  psdmul  22219  psdmvr  22222  psr1val  22236  vr1val  22242  ply1val  22244  coe1fval  22255  coe1fv  22256  coe1tmmul2  22327  coe1tmmul  22328  coe1tmmul2fv  22329  coe1pwmulfv  22331  evls1val  22371  evl1fval  22379  evl1val  22380  mamulid  22489  mamurid  22490  mdetleib  22635  mdetleib1  22639  mdetunilem9  22668  mdetuni0  22669  mdetmul  22671  cpmidpmatlem1  22918  ordtval  23237  cnpval  23284  ptpjpre1  23619  ptpjopn  23660  dfac14  23666  upxp  23671  uptx  23673  hauseqlcld  23694  txlm  23696  xkoptsub  23702  xkoinjcn  23735  kqval  23774  xpstopnlem1  23857  fmval  23991  flfval  24038  ptcmplem2  24101  ptcmplem3  24102  symgtgp  24154  qustgpopn  24168  ussval  24307  iscfilu  24335  ispsmet  24352  ismet  24371  isxmet  24372  mopnval  24486  prdsxmslem2  24577  nmfval  24636  nmval  24637  nmoval  24763  metdsval  24896  divcn  24918  mulc1cncf  24955  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25004  evth  25009  evth2  25010  lebnumlem3  25013  isphtpy  25031  isphtpc  25044  pcofval  25060  pcovalg  25062  pco1  25065  pcopt  25072  pcopt2  25073  pcoass  25074  pcorevcl  25075  pcorevlem  25076  pcorev2  25078  pi1xfrcnv  25107  cphnm  25243  tcphval  25268  tcphnmval  25279  cfilfval  25314  iscmet  25334  iscmet3lem3  25340  rrxval  25437  ehlval  25464  ivth2  25505  ovolval  25523  ovollb2lem  25538  ovolunlem1a  25546  ovolunlem1  25547  ovoliunlem1  25552  ovoliunlem2  25553  ovolicc1  25566  voliunlem1  25600  voliunlem2  25601  voliunlem3  25602  volsup  25606  ioorval  25624  uniioombllem3  25635  uniioombllem6  25638  volsup2  25655  volcn  25656  volivth  25657  vitalilem2  25659  vitalilem3  25660  vitalilem4  25661  vitali  25663  mbfmax  25699  mbfimaopnlem  25705  itg1val  25733  i1f1lem  25739  itg11  25741  itg1addlem4  25749  itg1mulc  25754  i1fres  25755  itg1climres  25764  mbfi1fseqlem2  25766  mbfi1fseqlem3  25767  mbfi1fseqlem6  25770  mbfi1flimlem  25772  mbfi1flim  25773  mbfmullem2  25774  itg2seq  25792  itg2uba  25793  itg2splitlem  25798  itg2monolem1  25800  itg2monolem2  25801  itg2monolem3  25802  itg2mono  25803  itg2i1fseqle  25804  itg2i1fseq  25805  itg2i1fseq2  25806  itg2addlem  25808  itg2cnlem1  25811  itg2cn  25813  limccnp2  25942  dvnff  25973  dvnp1  25975  cpnfval  25982  elcpn  25984  dvrec  26005  dvcnvlem  26026  dveflem  26029  dvef  26030  dvferm1  26035  dvferm2  26037  rolle  26040  dvlip  26043  dvlipcn  26044  dv11cn  26051  dvivthlem1  26058  dvivth  26060  lhop1lem  26063  ftc1lem1  26085  ftc1lem5  26090  ftc2  26094  itgsubstlem  26098  tdeglem3  26107  tdeglem4  26108  mdegval  26111  mdegmullem  26126  deg1fval  26128  deg1ldg  26140  deg1leb  26143  coe1mul3  26147  uc1pval  26188  mon1pval  26190  mon1pid  26202  q1pval  26203  r1pval  26206  ply1remlem  26213  ig1pval  26224  plyval  26241  elply2  26244  plyeq0lem  26258  coeval  26271  dgrval  26276  coeid2  26287  coemullem  26298  coemul  26300  plymulidp  26334  elqaalem1  26371  elqaalem2  26372  elqaalem3  26373  iaa  26377  aareccl  26378  aannenlem1  26380  geolim3  26391  aaliou3lem1  26394  aaliou3lem2  26395  aaliou3lem5  26399  aaliou3lem6  26400  aaliou3lem7  26401  aaliou3  26403  tayl0  26413  taylthlem1  26424  taylthlem2  26425  ulmshftlem  26440  ulmshft  26441  ulmuni  26443  ulmcau  26446  ulmdvlem1  26451  ulmdvlem3  26453  mtest  26455  mtestbdd  26456  mbfulm  26457  iblulm  26458  itgulm  26459  pserval  26461  pserval2  26462  radcnvlem1  26464  radcnvlem2  26465  dvradcnv  26472  pserulm  26473  pserdvlem2  26479  pserdv  26480  abelthlem1  26482  abelthlem3  26484  abelthlem4  26485  abelthlem5  26486  abelthlem6  26487  abelthlem7  26489  abelthlem8  26490  abelthlem9  26491  resinf1o  26589  efif1olem4  26598  eff1olem  26601  logcnlem5  26699  logtayllem  26712  logtayl  26713  logtaylsum  26714  logtayl2  26715  logccv  26716  asinval  26935  acosval  26936  atanval  26937  atantayl  26990  leibpilem2  26994  leibpi  26995  leibpisum  26996  log2cnv  26997  log2tlbnd  26998  areaval  27017  efrlim  27022  dfef2  27023  amgmlem  27042  emcllem2  27049  emcllem3  27050  emcllem4  27051  emcllem5  27052  emcllem6  27053  emcllem7  27054  zetacvg  27067  lgamgulmlem4  27084  lgamgulmlem5  27085  lgamgulm2  27088  lgamcvglem  27092  igamval  27099  lgamcvg2  27107  gamcvg2lem  27111  ftalem7  27131  basellem2  27134  basellem3  27135  basellem4  27136  basellem5  27137  basellem6  27138  basellem8  27140  basellem9  27141  chtval  27162  vmaval  27165  chpval  27174  ppival  27179  muval  27184  prmorcht  27230  sqff1o  27234  dvdsflsumcom  27240  musum  27243  muinv  27245  sgmppw  27249  fsumvma  27265  pclogsum  27267  dchrfi  27307  bposlem5  27340  bposlem7  27342  bposlem8  27343  bposlem9  27344  lgsfval  27354  lgsdir  27384  lgsdilem2  27385  lgsdi  27386  lgsne0  27387  lgsqrlem2  27399  lgsqrlem4  27401  lgseisenlem2  27428  dchrmusum2  27546  dchrvmasumlem1  27547  dchrvmasumiflem1  27553  dchrvmaeq0  27556  dchrisum0fval  27557  dchrisum0re  27565  mulog2sumlem1  27586  pntrval  27614  pntsval  27624  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntlem3  27661  abvcxp  27667  padicfval  27668  padicval  27669  padicabv  27682  ostth1  27685  ostth2  27689  ostth3  27690  nosupfv  27758  noinffv  27773  newval  27916  leftval  27930  rightval  27931  iscgrg  28669  legval  28741  ishpg  28916  iscgra  28966  isinag  28995  isleag  29004  iseqlg  29024  ttgval  29032  elee  29051  axsegconlem1  29075  axsegconlem9  29083  axsegconlem10  29084  axpasch  29099  axlowdimlem15  29114  axlowdim  29119  axeuclidlem  29120  axcontlem2  29123  eengv  29137  vtxval  29158  iedgval  29159  edgval  29207  vtxdgval  29626  wwlksnextinj  30056  wwlksnextsurj  30057  clwwlkfv  30207  clwwlknonmpo  30248  fusgreg2wsplem  30492  fusgreghash2wsp  30497  numclwwlk1lem2fv  30515  gidval  30672  grpoinvval  30683  bafval  30764  imsval  30845  dipfval  30862  sspval  30883  nmooval  30923  hmoval  30970  ipasslem8  30997  ipasslem9  30998  ipblnfi  31015  ubthlem2  31031  htthlem  31077  normval  31284  ocval  31440  occllem  31463  hsupval  31494  pjhfval  31556  pjhval  31557  chscllem2  31798  chscllem3  31799  hosval  31900  homval  31901  hodval  31902  hfsval  31903  hfmval  31904  brafval  32103  braval  32104  kbval  32114  eigvalval  32120  cnlnadjlem1  32227  nmopadjlei  32248  hmopidmchi  32311  strlem2  32411  hstrlem2  32419  cdj3lem2  32595  ofpreima  32828  psgnfzto1stlem  33241  evpmval  33286  altgnsg  33290  inftmrel  33321  isinftm  33322  qusker  33496  qusvscpbl  33498  qusvsval  33499  mxidlval  33610  idlsrgval  33660  psrmonmul  33808  dimval  33859  dimvalfi  33860  smatfval  34053  lmatval  34071  locfinreflem  34098  rspecval  34122  rmulccn  34186  xrmulc1cn  34188  xrge0iifcv  34192  xrge0iifiso  34193  xrge0iifhom  34195  xrge0iif1  34196  qqhval  34230  rrhval  34254  xrhval  34276  ddeval1  34492  ddeval0  34493  sxbrsigalem0  34529  sxbrsigalem3  34530  eulerpartlemgv  34631  rrvmbfm  34700  dstrvval  34729  coinflippv  34742  ballotlem2  34747  ballotlemfval  34748  ballotlemi  34759  ballotlemsval  34767  ballotlemrval  34776  ballotth  34796  signstfv  34818  signsvvfval  34833  onvf1odlem3  35409  derangval  35478  subfacval  35484  erdszelem3  35504  erdszelem9  35510  erdszelem10  35511  txpconn  35543  indispconn  35545  cvxpconn  35553  cvmlift2lem2  35615  cvmlift2lem3  35616  cvmlift2lem7  35620  cvmliftphtlem  35628  cvmlift3lem4  35633  snmlfval  35641  snmlval  35642  gonafv  35661  mvtval  35811  mrsubffval  35818  mrsubcv  35821  mrsubrn  35824  elmrsubrn  35831  msubffval  35834  mvhval  35845  mpstval  35846  mstaval  35855  mclsval  35874  mppsval  35883  sinccvglem  35983  circum  35985  divcnvlin  36044  iprodefisum  36052  iprodgam  36053  faclimlem1  36054  faclimlem2  36055  faclim  36057  iprodfac  36058  faclim2  36059  dfrdg2  36104  findabrcl  36775  dnival  36870  bj-evalval  37526  bj-inftyexpitaudisj  37658  bj-inftyexpiinv  37661  bj-inftyexpidisj  37663  curfv  38060  finixpnum  38065  poimirlem16  38096  poimir  38113  broucube  38114  mblfinlem2  38118  voliunnfl  38124  volsupnfl  38125  itg2addnclem  38131  itg2addnclem3  38133  ftc1cnnc  38152  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anc  38161  ftc2nc  38162  fvopabf4g  38182  sdclem2  38202  fdc  38205  lmclim2  38218  geomcau  38219  istotbnd  38229  isbnd  38240  prdsbnd2  38255  heiborlem6  38276  heiborlem7  38277  heiborlem8  38278  rrnval  38287  rrncmslem  38292  idlval  38473  pridlval  38493  maxidlval  38499  lshpset  39563  lsatset  39575  lcvfbr  39605  lflset  39644  lflnegcl  39660  lshpkrlem1  39695  lshpkrlem2  39696  lshpkrlem3  39697  ldualset  39710  cmtfvalN  39795  cvrfval  39853  pats  39870  llnset  40090  lplnset  40114  lvolset  40157  lineset  40323  pointsetN  40326  psubspset  40329  pmapval  40342  paddfval  40382  pclfvalN  40474  polfvalN  40489  polvalN  40490  psubclsetN  40521  watvalN  40578  lhpset  40580  lautset  40667  pautsetN  40683  ldilset  40694  ltrnset  40703  dilsetN  40738  trnsetN  40741  trlset  40746  trlval  40747  tgrpset  41330  tendoset  41344  tendo02  41372  erngset  41385  erngset-rN  41393  cdlemksv  41429  dvaset  41590  dvaplusgv  41595  diafval  41616  diaval  41617  dvhset  41666  cdlemm10N  41703  docafvalN  41707  djafvalN  41719  dibfval  41726  dibval  41727  dicfval  41760  dicval  41761  dihval  41817  dochfval  41935  djhfval  41982  dochfl1  42061  lpolsetN  42067  lcdval  42174  mapdhval  42309  hvmapfval  42344  hdmap1fval  42381  fimgmcyc  43113  prjspval  43146  isnacs  43246  mzpclval  43267  mzpsubst  43290  mzprename  43291  mzpcompact2lem  43293  eldiophb  43299  diophrw  43301  eldioph2  43304  diophin  43314  diophun  43315  diophren  43351  pell1qrval  43384  pell14qrval  43386  pell1234qrval  43388  pellfundval  43418  rmxypairf1o  43449  rmxyval  43453  mzpcong  43510  pw2f1ocnv  43575  dnnumch1  43582  dfac11  43600  hbtlem1  43661  hbtlem7  43663  elmnc  43674  dgraaval  43682  mpaaval  43689  itgoval  43699  flcidc  43708  mendval  43717  cytpval  43740  cantnfub  43859  cantnfresb  43862  tfsconcatrev  43886  elcnvlem  44138  comptiunov2i  44243  dftrcl3  44257  trclfvcom  44260  cnvtrclfv  44261  cotrcltrcl  44262  trclimalb2  44263  trclfvdecomr  44265  dfrtrcl3  44270  dfrtrcl4  44275  clsk1indlem0  44578  clsk1indlem2  44579  clsk1indlem3  44580  clsk1indlem4  44581  clsk1indlem1  44582  k0004val  44687  lhe4.4ex1a  44866  addrfv  45005  subrfv  45006  mulvfv  45007  monoord2xrv  46018  sumnnodd  46167  liminfgval  46297  ioodvbdlimc2lem  46469  itgsin0pilem1  46485  stoweidlem55  46590  wallispilem1  46600  wallispilem2  46601  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  dirkerval  46626  fourierdlem2  46644  fourierdlem3  46645  fourierdlem29  46671  fourierdlem62  46703  fourierdlem80  46721  fourierdlem103  46744  fourierdlem104  46745  fourierswlem  46765  fouriersw  46766  iundjiunlem  46994  carageniuncllem2  47057  0ome  47064  hoidmv1le  47129  hoidmvlelem3  47132  smflimsuplem7  47361  nthrucw  47423  iccpval  47982  fppr  48309  bigoval  49132  ackval0  49263  ackval41a  49277  eenglngeehlnm  49322  oppcinito  49817  oppctermo  49818  dfinito4  50083  prstcval  50133  mndtcval  50161  setc1onsubc  50184  lmdfval2  50237  cmdfval2  50238  vsetrec  50285  onsetreclem1  50287  elpglem3  50295  pgindnf  50298  sinhval-named  50318  coshval-named  50319  tanhval-named  50320  secval  50329  cscval  50330  cotval  50331  aacllem  50383