Theorem fvmpt 6987

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ↦ cmpt 5193  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6490  df-fun 6536  df-fv 6542

This theorem is referenced by:  fvmptex  7002  fvmptrabfv  7020  mptfvmpt  7224  fvmptopab  7463  ofval  7683  caofinvl  7704  fvresex  7953  1stval  7984  2ndval  7985  reldm  8037  curry1val  8096  curry2val  8100  fsplitfpar  8109  fnwelem  8123  brtpos2  8224  onovuni  8325  tz7.44-1  8389  oasuc  8505  oesuclem  8506  omsuc  8507  onasuc  8509  onmsuc  8510  fsetfocdm  8854  fvmptmap  8875  xpcomco  9051  unxpdomlem1  9212  unfilem2  9262  ordtypelem3  9478  ixpiunwdom  9548  inf3lema  9589  noinfep  9625  cantnfval  9633  cantnflem1d  9653  cantnflem1  9654  ssttrcl  9680  ttrcltr  9681  ttrclselem2  9691  r1sucg  9737  r0weon  9992  infxpenc2lem1  9999  fseqenlem1  10004  fseqenlem2  10005  dfac8alem  10009  ac5num  10016  acni2  10026  dfac4  10102  dfac2a  10109  dfacacn  10121  dfac12lem1  10123  ackbij1lem7  10204  ackbij2lem2  10218  ackbij2lem3  10219  cfsmolem  10250  fin23lem28  10320  fin23lem39  10330  isf32lem6  10338  isf32lem7  10339  isf32lem8  10340  fin1a2lem3  10382  itunifval  10396  itunisuc  10399  axdc2lem  10428  axdc3lem2  10431  axcclem  10437  zorn2lem1  10476  negiso  12191  infrenegsup  12194  uzval  12860  flval  13823  ceilval  13867  ceilval2  13869  monoord2  14065  seqf1olem2  14074  seqf1o  14075  seqdistr  14085  serle  14089  seqof  14091  swrdfv  14682  revval  14793  revfv  14796  wwlktovf1  14990  wwlktovfo  14991  sgnval  15121  cjval  15149  reval  15153  imval  15154  sqrtval  15284  absval  15285  limsupval  15521  limsupgval  15523  climmpt  15618  climle  15687  rlimdiv  15693  isercolllem1  15712  isercoll2  15716  caurcvg2  15725  fsumser  15777  isumadd  15814  fsumcnv  15820  fsumrev  15826  fsumshft  15827  iserabs  15863  cvgcmp  15864  cvgcmpce  15866  incexclem  15886  isumless  15895  divcnvshft  15905  supcvg  15906  harmonic  15909  trireciplem  15912  trirecip  15913  expcnv  15914  explecnv  15915  geolim  15920  geolim2  15921  geo2lim  15925  geomulcvg  15926  geoisum  15927  geoisumr  15928  geoisum1  15929  geoisum1c  15930  cvgrat  15933  mertenslem2  15935  mertens  15936  prodfdiv  15946  fprodser  15999  fprodshft  16026  fprodrev  16027  fprodcnv  16033  iprodmul  16053  bpolylem  16098  eftval  16126  efval  16129  efcvgfsum  16136  ege2le3  16140  eftlub  16161  eflegeo  16173  sinval  16174  cosval  16175  tanval  16180  eirrlem  16256  rpnnen2lem1  16266  rpnnen2lem2  16267  bitsfval  16477  bitsinv2  16497  bitsinv  16502  sadcf  16507  sadc0  16508  sadcp1  16509  smupf  16532  smup0  16533  smupp1  16534  qnumval  16792  qdenval  16793  phival  16822  crth  16833  phimullem  16834  eulerthlem2  16837  phisum  16846  odzval  16847  iserodd  16891  pcmpt  16948  prmreclem1  16972  prmreclem2  16973  prmreclem4  16975  prmreclem5  16976  prmreclem6  16977  1arithlem1  16979  1arithlem2  16980  vdwapfval  17027  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  vdwlem9  17045  ramub1lem2  17083  ramcl  17085  prmoval  17089  strfvnd  17241  topnval  17483  prdsplusgfval  17523  prdsmulrfval  17525  isacs  17703  acsfn  17711  homffval  17742  comfffval  17750  oppcval  17765  monfval  17785  oppcmon  17791  sectffval  17803  invffval  17811  isoval  17818  idfuval  17929  homafval  18082  arwval  18096  coafval  18117  yonedainv  18333  oduval  18340  pltfval  18381  lubfval  18400  lubval  18406  glbfval  18413  glbval  18419  p0val  18477  p1val  18478  ipoval  18582  plusffval  18700  grpidval  18715  issubmgm  18756  issubm  18857  prdspjmhm  18884  efmnd  18925  smndex1gbas  18957  smndex1gid  18959  smndex1igid  18961  smndex1igidOLD  18962  grpinvfval  19041  grpinvval  19043  grpsubfval  19046  grpsubfvalALT  19047  grplactval  19104  prdsinvlem  19111  mulgfval  19131  mulgfvalALT  19132  pwsmulg  19181  issubg  19188  isnsg  19217  cycsubmel  19267  cycsubgcl  19273  conjghm  19315  conjnmz  19318  cntrval  19385  cntzfval  19386  cntzval  19387  oppgval  19413  psgnfval  19566  psgnval  19573  odfval  19598  odval  19600  sylow1lem4  19667  pgpssslw  19680  sylow2blem3  19688  sylow3lem2  19694  lsmfval  19704  pj1fval  19760  efgval  19783  efgsval  19797  frgpval  19824  vrgpval  19833  mulgmhm  19893  mulgghm  19894  ablfaclem1  20153  mgpval  20215  srglmhm  20299  srgrmhm  20300  ringlghm  20391  ringrghm  20392  pwspjmhmmgpd  20405  pwsexpg  20406  opprval  20416  dvdsrval  20439  isunit  20451  invrfval  20467  dvrfval  20480  isirred  20497  issubrng  20628  issubrg  20652  rgspnval  20693  rrgval  20778  fidomndrnglem  20850  issdrg  20865  abvfval  20887  abvtrivd  20909  staffval  20918  stafval  20919  scaffval  20975  lmodvsghm  21018  lssset  21028  lspfval  21068  islbs  21171  sraval  21270  rlmval  21286  2idlval  21357  lpival  21457  expmhm  21551  expghm  21590  mulgghm2  21591  mulgrhm  21592  zrhval  21622  zrhmulg  21624  zlmval  21630  chrval  21638  znval  21650  znzrhval  21661  evpmss  21701  psgnevpmb  21702  ip0l  21751  ipffval  21763  ocvfval  21781  ocvval  21782  cssval  21797  thlval  21810  pjfval  21821  pjval  21825  isobs  21835  prdsinvgd2  21857  uvcresum  21908  frlmup1  21913  frlmup2  21914  islinds  21924  islindf5  21954  aspval  21987  asclval  21994  psrmulval  22059  psrlidm  22076  psrridm  22077  psrascl  22093  mvrval  22096  mvrval2  22097  mplmonmul  22152  evlslem3  22196  evlslem1  22198  evlsval  22202  evlssca  22210  evlsvar  22211  psdmul  22294  psdmvr  22297  psr1val  22311  vr1val  22317  ply1val  22319  coe1fval  22330  coe1fv  22331  coe1tmmul2  22402  coe1tmmul  22403  coe1tmmul2fv  22404  coe1pwmulfv  22406  evls1val  22445  evl1fval  22453  evl1val  22454  mamulid  22563  mamurid  22564  mdetleib  22709  mdetleib1  22713  mdetunilem9  22742  mdetuni0  22743  mdetmul  22745  cpmidpmatlem1  22992  ordtval  23311  cnpval  23358  ptpjpre1  23693  ptpjopn  23734  dfac14  23740  upxp  23745  uptx  23747  hauseqlcld  23768  txlm  23770  xkoptsub  23776  xkoinjcn  23809  kqval  23848  xpstopnlem1  23931  fmval  24065  flfval  24112  ptcmplem2  24175  ptcmplem3  24176  symgtgp  24228  qustgpopn  24242  ussval  24381  iscfilu  24409  ispsmet  24426  ismet  24445  isxmet  24446  mopnval  24560  prdsxmslem2  24651  nmfval  24710  nmval  24711  nmoval  24837  metdsval  24970  divcn  24992  mulc1cncf  25029  icopnfhmeo  25067  iccpnfhmeo  25069  xrhmeo  25070  cnheiborlem  25078  evth  25083  evth2  25084  lebnumlem3  25087  isphtpy  25105  isphtpc  25118  pcofval  25134  pcovalg  25136  pco1  25139  pcopt  25146  pcopt2  25147  pcoass  25148  pcorevcl  25149  pcorevlem  25150  pcorev2  25152  pi1xfrcnv  25181  cphnm  25317  tcphval  25342  tcphnmval  25353  cfilfval  25388  iscmet  25408  iscmet3lem3  25414  rrxval  25511  ehlval  25538  ivth2  25579  ovolval  25597  ovollb2lem  25612  ovolunlem1a  25620  ovolunlem1  25621  ovoliunlem1  25626  ovoliunlem2  25627  ovolicc1  25640  voliunlem1  25674  voliunlem2  25675  voliunlem3  25676  volsup  25680  ioorval  25698  uniioombllem3  25709  uniioombllem6  25712  volsup2  25729  volcn  25730  volivth  25731  vitalilem2  25733  vitalilem3  25734  vitalilem4  25735  vitali  25737  mbfmax  25773  mbfimaopnlem  25779  itg1val  25807  i1f1lem  25813  itg11  25815  itg1addlem4  25823  itg1mulc  25828  i1fres  25829  itg1climres  25838  mbfi1fseqlem2  25840  mbfi1fseqlem3  25841  mbfi1fseqlem6  25844  mbfi1flimlem  25846  mbfi1flim  25847  mbfmullem2  25848  itg2seq  25866  itg2uba  25867  itg2splitlem  25872  itg2monolem1  25874  itg2monolem2  25875  itg2monolem3  25876  itg2mono  25877  itg2i1fseqle  25878  itg2i1fseq  25879  itg2i1fseq2  25880  itg2addlem  25882  itg2cnlem1  25885  itg2cn  25887  limccnp2  26016  dvnff  26047  dvnp1  26049  cpnfval  26056  elcpn  26058  dvrec  26079  dvcnvlem  26100  dveflem  26103  dvef  26104  dvferm1  26109  dvferm2  26111  rolle  26114  dvlip  26117  dvlipcn  26118  dv11cn  26125  dvivthlem1  26132  dvivth  26134  lhop1lem  26137  ftc1lem1  26159  ftc1lem5  26164  ftc2  26168  itgsubstlem  26172  tdeglem3  26181  tdeglem4  26182  mdegval  26185  mdegmullem  26200  deg1fval  26202  deg1ldg  26214  deg1leb  26217  coe1mul3  26221  uc1pval  26262  mon1pval  26264  mon1pid  26276  q1pval  26277  r1pval  26280  ply1remlem  26287  ig1pval  26298  plyval  26315  elply2  26318  plyeq0lem  26332  coeval  26345  dgrval  26350  coeid2  26361  coemullem  26372  coemul  26374  plymulidp  26408  elqaalem1  26445  elqaalem2  26446  elqaalem3  26447  iaa  26451  aareccl  26452  aannenlem1  26454  geolim3  26465  aaliou3lem1  26468  aaliou3lem2  26469  aaliou3lem5  26473  aaliou3lem6  26474  aaliou3lem7  26475  aaliou3  26477  tayl0  26487  taylthlem1  26498  taylthlem2  26499  ulmshftlem  26514  ulmshft  26515  ulmuni  26517  ulmcau  26520  ulmdvlem1  26525  ulmdvlem3  26527  mtest  26529  mtestbdd  26530  mbfulm  26531  iblulm  26532  itgulm  26533  pserval  26535  pserval2  26536  radcnvlem1  26538  radcnvlem2  26539  dvradcnv  26546  pserulm  26547  pserdvlem2  26553  pserdv  26554  abelthlem1  26556  abelthlem3  26558  abelthlem4  26559  abelthlem5  26560  abelthlem6  26561  abelthlem7  26563  abelthlem8  26564  abelthlem9  26565  resinf1o  26663  efif1olem4  26672  eff1olem  26675  logcnlem5  26773  logtayllem  26786  logtayl  26787  logtaylsum  26788  logtayl2  26789  logccv  26790  asinval  27009  acosval  27010  atanval  27011  atantayl  27064  leibpilem2  27068  leibpi  27069  leibpisum  27070  log2cnv  27071  log2tlbnd  27072  areaval  27091  efrlim  27096  dfef2  27097  amgmlem  27116  emcllem2  27123  emcllem3  27124  emcllem4  27125  emcllem5  27126  emcllem6  27127  emcllem7  27128  zetacvg  27141  lgamgulmlem4  27158  lgamgulmlem5  27159  lgamgulm2  27162  lgamcvglem  27166  igamval  27173  lgamcvg2  27181  gamcvg2lem  27185  ftalem7  27205  basellem2  27208  basellem3  27209  basellem4  27210  basellem5  27211  basellem6  27212  basellem8  27214  basellem9  27215  chtval  27236  vmaval  27239  chpval  27248  ppival  27253  muval  27258  prmorcht  27304  sqff1o  27308  dvdsflsumcom  27314  musum  27317  muinv  27319  sgmppw  27323  fsumvma  27339  pclogsum  27341  dchrfi  27381  bposlem5  27414  bposlem7  27416  bposlem8  27417  bposlem9  27418  lgsfval  27428  lgsdir  27458  lgsdilem2  27459  lgsdi  27460  lgsne0  27461  lgsqrlem2  27473  lgsqrlem4  27475  lgseisenlem2  27502  dchrmusum2  27620  dchrvmasumlem1  27621  dchrvmasumiflem1  27627  dchrvmaeq0  27630  dchrisum0fval  27631  dchrisum0re  27639  mulog2sumlem1  27660  pntrval  27688  pntsval  27698  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  pntlem3  27735  abvcxp  27741  padicfval  27742  padicval  27743  padicabv  27756  ostth1  27759  ostth2  27763  ostth3  27764  nosupfv  27832  noinffv  27847  newval  27990  leftval  28004  rightval  28005  iscgrg  28743  legval  28815  ishpg  28996  iscgra  29073  isinag  29106  isleag  29115  iseqlg  29135  ttgval  29161  elee  29180  axsegconlem1  29204  axsegconlem9  29212  axsegconlem10  29213  axpasch  29228  axlowdimlem15  29243  axlowdim  29248  axeuclidlem  29249  axcontlem2  29252  eengv  29266  vtxval  29287  iedgval  29288  edgval  29336  vtxdgval  29755  wwlksnextinj  30185  wwlksnextsurj  30186  clwwlkfv  30336  clwwlknonmpo  30377  fusgreg2wsplem  30621  fusgreghash2wsp  30626  numclwwlk1lem2fv  30644  gidval  30801  grpoinvval  30812  bafval  30893  imsval  30974  dipfval  30991  sspval  31012  nmooval  31052  hmoval  31099  ipasslem8  31126  ipasslem9  31127  ipblnfi  31144  ubthlem2  31160  htthlem  31206  normval  31413  ocval  31569  occllem  31592  hsupval  31623  pjhfval  31685  pjhval  31686  chscllem2  31927  chscllem3  31928  hosval  32029  homval  32030  hodval  32031  hfsval  32032  hfmval  32033  brafval  32232  braval  32233  kbval  32243  eigvalval  32249  cnlnadjlem1  32356  nmopadjlei  32377  hmopidmchi  32440  strlem2  32540  hstrlem2  32548  cdj3lem2  32724  ofpreima  32947  psgnfzto1stlem  33357  evpmval  33402  altgnsg  33406  inftmrel  33437  isinftm  33438  qusker  33608  qusvscpbl  33610  qusvsval  33611  mxidlval  33685  idlsrgval  33734  psrmonmul  33881  dimval  33932  dimvalfi  33933  smatfval  34126  lmatval  34144  locfinreflem  34171  rspecval  34195  rmulccn  34259  xrmulc1cn  34261  xrge0iifcv  34265  xrge0iifiso  34266  xrge0iifhom  34268  xrge0iif1  34269  qqhval  34303  rrhval  34327  xrhval  34349  ddeval1  34565  ddeval0  34566  sxbrsigalem0  34602  sxbrsigalem3  34603  eulerpartlemgv  34704  rrvmbfm  34773  dstrvval  34802  coinflippv  34815  ballotlem2  34820  ballotlemfval  34821  ballotlemi  34832  ballotlemsval  34840  ballotlemrval  34849  ballotth  34869  signstfv  34891  signsvvfval  34906  onvf1odlem3  35484  derangval  35554  subfacval  35560  erdszelem3  35580  erdszelem9  35586  erdszelem10  35587  txpconn  35619  indispconn  35621  cvxpconn  35629  cvmlift2lem2  35691  cvmlift2lem3  35692  cvmlift2lem7  35696  cvmliftphtlem  35704  cvmlift3lem4  35709  snmlfval  35717  snmlval  35718  gonafv  35737  mvtval  35887  mrsubffval  35894  mrsubcv  35897  mrsubrn  35900  elmrsubrn  35907  msubffval  35910  mvhval  35921  mpstval  35922  mstaval  35931  mclsval  35950  mppsval  35959  sinccvglem  36059  circum  36061  divcnvlin  36120  iprodefisum  36128  iprodgam  36129  faclimlem1  36130  faclimlem2  36131  faclim  36133  iprodfac  36134  faclim2  36135  dfrdg2  36180  findabrcl  36850  dnival  36945  bj-evalval  37600  bj-inftyexpitaudisj  37732  bj-inftyexpiinv  37735  bj-inftyexpidisj  37737  curfv  38134  finixpnum  38139  poimirlem16  38170  poimir  38187  broucube  38188  mblfinlem2  38192  voliunnfl  38198  volsupnfl  38199  itg2addnclem  38205  itg2addnclem3  38207  ftc1cnnc  38226  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anc  38235  ftc2nc  38236  fvopabf4g  38256  sdclem2  38276  fdc  38279  lmclim2  38292  geomcau  38293  istotbnd  38303  isbnd  38314  prdsbnd2  38329  heiborlem6  38350  heiborlem7  38351  heiborlem8  38352  rrnval  38361  rrncmslem  38366  idlval  38547  pridlval  38567  maxidlval  38573  lshpset  39637  lsatset  39649  lcvfbr  39679  lflset  39718  lflnegcl  39734  lshpkrlem1  39769  lshpkrlem2  39770  lshpkrlem3  39771  ldualset  39784  cmtfvalN  39869  cvrfval  39927  pats  39944  llnset  40164  lplnset  40188  lvolset  40231  lineset  40397  pointsetN  40400  psubspset  40403  pmapval  40416  paddfval  40456  pclfvalN  40548  polfvalN  40563  polvalN  40564  psubclsetN  40595  watvalN  40652  lhpset  40654  lautset  40741  pautsetN  40757  ldilset  40768  ltrnset  40777  dilsetN  40812  trnsetN  40815  trlset  40820  trlval  40821  tgrpset  41404  tendoset  41418  tendo02  41446  erngset  41459  erngset-rN  41467  cdlemksv  41503  dvaset  41664  dvaplusgv  41669  diafval  41690  diaval  41691  dvhset  41740  cdlemm10N  41777  docafvalN  41781  djafvalN  41793  dibfval  41800  dibval  41801  dicfval  41834  dicval  41835  dihval  41891  dochfval  42009  djhfval  42056  dochfl1  42135  lpolsetN  42141  lcdval  42248  mapdhval  42383  hvmapfval  42418  hdmap1fval  42455  fimgmcyc  43189  prjspval  43222  isnacs  43322  mzpclval  43343  mzpsubst  43366  mzprename  43367  mzpcompact2lem  43369  eldiophb  43375  diophrw  43377  eldioph2  43380  diophin  43390  diophun  43391  diophren  43427  pell1qrval  43460  pell14qrval  43462  pell1234qrval  43464  pellfundval  43494  rmxypairf1o  43525  rmxyval  43529  mzpcong  43586  pw2f1ocnv  43651  dnnumch1  43658  dfac11  43676  hbtlem1  43737  hbtlem7  43739  elmnc  43750  dgraaval  43758  mpaaval  43765  itgoval  43775  flcidc  43784  mendval  43793  cytpval  43816  cantnfub  43935  cantnfresb  43938  tfsconcatrev  43962  elcnvlem  44214  comptiunov2i  44319  dftrcl3  44333  trclfvcom  44336  cnvtrclfv  44337  cotrcltrcl  44338  trclimalb2  44339  trclfvdecomr  44341  dfrtrcl3  44346  dfrtrcl4  44351  clsk1indlem0  44654  clsk1indlem2  44655  clsk1indlem3  44656  clsk1indlem4  44657  clsk1indlem1  44658  k0004val  44763  lhe4.4ex1a  44926  addrfv  45064  subrfv  45065  mulvfv  45066  monoord2xrv  46084  sumnnodd  46233  liminfgval  46363  ioodvbdlimc2lem  46535  itgsin0pilem1  46551  stoweidlem55  46656  wallispilem1  46666  wallispilem2  46667  wallispilem4  46669  wallispi2lem1  46672  wallispi2lem2  46673  dirkerval  46692  fourierdlem2  46710  fourierdlem3  46711  fourierdlem29  46737  fourierdlem62  46769  fourierdlem80  46787  fourierdlem103  46810  fourierdlem104  46811  fourierswlem  46831  fouriersw  46832  iundjiunlem  47060  carageniuncllem2  47123  0ome  47130  hoidmv1le  47195  hoidmvlelem3  47198  smflimsuplem7  47427  nthrucw  47489  iccpval  48048  fppr  48375  bigoval  49209  ackval0  49340  ackval41a  49354  eenglngeehlnm  49399  oppcinito  49893  oppctermo  49894  dfinito4  50159  prstcval  50209  mndtcval  50237  setc1onsubc  50260  lmdfval2  50313  cmdfval2  50314  vsetrec  50361  onsetreclem1  50363  elpglem3  50371  pgindnf  50374  sinhval-named  50394  coshval-named  50395  tanhval-named  50396  secval  50405  cscval  50406  cotval  50407  aacllem  50470