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 697	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ↦ cmpt 5153  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493

This theorem is referenced by:  fvmptex  6950  fvmptrabfv  6968  mptfvmpt  7172  fvmptopab  7411  ofval  7631  caofinvl  7652  fvresex  7902  1stval  7933  2ndval  7934  reldm  7986  curry1val  8044  curry2val  8048  fsplitfpar  8057  fnwelem  8071  brtpos2  8172  onovuni  8272  tz7.44-1  8335  oasuc  8449  oesuclem  8450  omsuc  8451  onasuc  8453  onmsuc  8454  fsetfocdm  8798  fvmptmap  8819  xpcomco  8995  unxpdomlem1  9156  unfilem2  9206  ordtypelem3  9425  ixpiunwdom  9495  inf3lema  9536  noinfep  9572  cantnfval  9580  cantnflem1d  9600  cantnflem1  9601  ssttrcl  9627  ttrcltr  9628  ttrclselem2  9638  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  12127  infrenegsup  12130  uzval  12781  flval  13744  ceilval  13788  ceilval2  13790  monoord2  13986  seqf1olem2  13995  seqf1o  13996  seqdistr  14006  serle  14010  seqof  14012  swrdfv  14602  revval  14713  revfv  14716  wwlktovf1  14910  wwlktovfo  14911  sgnval  15041  cjval  15055  reval  15059  imval  15060  sqrtval  15190  absval  15191  limsupval  15427  limsupgval  15429  climmpt  15524  climle  15593  rlimdiv  15599  isercolllem1  15618  isercoll2  15622  caurcvg2  15631  fsumser  15683  isumadd  15720  fsumcnv  15726  fsumrev  15732  fsumshft  15733  iserabs  15769  cvgcmp  15770  cvgcmpce  15772  incexclem  15792  isumless  15801  divcnvshft  15811  supcvg  15812  harmonic  15815  trireciplem  15818  trirecip  15819  expcnv  15820  explecnv  15821  geolim  15826  geolim2  15827  geo2lim  15831  geomulcvg  15832  geoisum  15833  geoisumr  15834  geoisum1  15835  geoisum1c  15836  cvgrat  15839  mertenslem2  15841  mertens  15842  prodfdiv  15852  fprodser  15905  fprodshft  15932  fprodrev  15933  fprodcnv  15939  iprodmul  15959  bpolylem  16004  eftval  16032  efval  16035  efcvgfsum  16042  ege2le3  16046  eftlub  16067  eflegeo  16079  sinval  16080  cosval  16081  tanval  16086  eirrlem  16162  rpnnen2lem1  16172  rpnnen2lem2  16173  bitsfval  16383  bitsinv2  16403  bitsinv  16408  sadcf  16413  sadc0  16414  sadcp1  16415  smupf  16438  smup0  16439  smupp1  16440  qnumval  16698  qdenval  16699  phival  16728  crth  16739  phimullem  16740  eulerthlem2  16743  phisum  16752  odzval  16753  iserodd  16797  pcmpt  16854  prmreclem1  16878  prmreclem2  16879  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  1arithlem1  16885  1arithlem2  16886  vdwapfval  16933  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  ramub1lem2  16989  ramcl  16991  prmoval  16995  strfvnd  17146  topnval  17388  prdsplusgfval  17428  prdsmulrfval  17430  isacs  17608  acsfn  17616  homffval  17647  comfffval  17655  oppcval  17670  monfval  17690  oppcmon  17696  sectffval  17708  invffval  17716  isoval  17723  idfuval  17834  homafval  17987  arwval  18001  coafval  18022  yonedainv  18238  oduval  18245  pltfval  18286  lubfval  18305  lubval  18311  glbfval  18318  glbval  18324  p0val  18382  p1val  18383  ipoval  18487  plusffval  18605  grpidval  18620  issubmgm  18661  issubm  18762  prdspjmhm  18788  efmnd  18829  smndex1gbas  18861  smndex1gid  18863  smndex1igid  18865  smndex1igidOLD  18866  grpinvfval  18945  grpinvval  18947  grpsubfval  18950  grpsubfvalALT  18951  grplactval  19009  prdsinvlem  19016  mulgfval  19036  mulgfvalALT  19037  pwsmulg  19086  issubg  19093  isnsg  19121  cycsubmel  19166  cycsubgcl  19172  conjghm  19215  conjnmz  19218  cntrval  19285  cntzfval  19286  cntzval  19287  oppgval  19313  psgnfval  19466  psgnval  19473  odfval  19498  odval  19500  sylow1lem4  19567  pgpssslw  19580  sylow2blem3  19588  sylow3lem2  19594  lsmfval  19604  pj1fval  19660  efgval  19683  efgsval  19697  frgpval  19724  vrgpval  19733  mulgmhm  19793  mulgghm  19794  ablfaclem1  20053  mgpval  20115  srglmhm  20193  srgrmhm  20194  ringlghm  20284  ringrghm  20285  pwspjmhmmgpd  20298  pwsexpg  20299  opprval  20309  dvdsrval  20332  isunit  20344  invrfval  20360  dvrfval  20373  isirred  20390  issubrng  20519  issubrg  20543  rgspnval  20584  rrgval  20669  fidomndrnglem  20744  issdrg  20760  abvfval  20782  abvtrivd  20804  staffval  20813  stafval  20814  scaffval  20870  lmodvsghm  20913  lssset  20923  lspfval  20963  islbs  21066  sraval  21165  rlmval  21181  2idlval  21244  lpival  21317  expmhm  21411  expghm  21450  mulgghm2  21451  mulgrhm  21452  zrhval  21482  zrhmulg  21484  zlmval  21490  chrval  21498  znval  21510  znzrhval  21521  evpmss  21561  psgnevpmb  21562  ip0l  21611  ipffval  21623  ocvfval  21641  ocvval  21642  cssval  21657  thlval  21670  pjfval  21681  pjval  21685  isobs  21695  prdsinvgd2  21717  uvcresum  21768  frlmup1  21773  frlmup2  21774  islinds  21784  islindf5  21814  aspval  21847  asclval  21854  psrmulval  21919  psrlidm  21936  psrridm  21937  psrascl  21953  mvrval  21956  mvrval2  21957  mplmonmul  22012  evlslem3  22056  evlslem1  22058  evlsval  22062  evlssca  22070  evlsvar  22071  psdmul  22154  psdmvr  22157  psr1val  22171  vr1val  22177  ply1val  22179  coe1fval  22190  coe1fv  22191  coe1tmmul2  22262  coe1tmmul  22263  coe1tmmul2fv  22264  coe1pwmulfv  22266  evls1val  22306  evl1fval  22314  evl1val  22315  mamulid  22424  mamurid  22425  mdetleib  22570  mdetleib1  22574  mdetunilem9  22603  mdetuni0  22604  mdetmul  22606  cpmidpmatlem1  22853  ordtval  23172  cnpval  23219  ptpjpre1  23554  ptpjopn  23595  dfac14  23601  upxp  23606  uptx  23608  hauseqlcld  23629  txlm  23631  xkoptsub  23637  xkoinjcn  23670  kqval  23709  xpstopnlem1  23792  fmval  23926  flfval  23973  ptcmplem2  24036  ptcmplem3  24037  symgtgp  24089  qustgpopn  24103  ussval  24242  iscfilu  24270  ispsmet  24287  ismet  24306  isxmet  24307  mopnval  24421  prdsxmslem2  24512  nmfval  24571  nmval  24572  nmoval  24698  metdsval  24831  divcn  24853  mulc1cncf  24890  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  cnheiborlem  24939  evth  24944  evth2  24945  lebnumlem3  24948  isphtpy  24966  isphtpc  24979  pcofval  24995  pcovalg  24997  pco1  25000  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevcl  25010  pcorevlem  25011  pcorev2  25013  pi1xfrcnv  25042  cphnm  25178  tcphval  25203  tcphnmval  25214  cfilfval  25249  iscmet  25269  iscmet3lem3  25275  rrxval  25372  ehlval  25399  ivth2  25440  ovolval  25458  ovollb2lem  25473  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliunlem2  25488  ovolicc1  25501  voliunlem1  25535  voliunlem2  25536  voliunlem3  25537  volsup  25541  ioorval  25559  uniioombllem3  25570  uniioombllem6  25573  volsup2  25590  volcn  25591  volivth  25592  vitalilem2  25594  vitalilem3  25595  vitalilem4  25596  vitali  25598  mbfmax  25634  mbfimaopnlem  25640  itg1val  25668  i1f1lem  25674  itg11  25676  itg1addlem4  25684  itg1mulc  25689  i1fres  25690  itg1climres  25699  mbfi1fseqlem2  25701  mbfi1fseqlem3  25702  mbfi1fseqlem6  25705  mbfi1flimlem  25707  mbfi1flim  25708  mbfmullem2  25709  itg2seq  25727  itg2uba  25728  itg2splitlem  25733  itg2monolem1  25735  itg2monolem2  25736  itg2monolem3  25737  itg2mono  25738  itg2i1fseqle  25739  itg2i1fseq  25740  itg2i1fseq2  25741  itg2addlem  25743  itg2cnlem1  25746  itg2cn  25748  limccnp2  25877  dvnff  25908  dvnp1  25910  cpnfval  25917  elcpn  25919  dvrec  25940  dvcnvlem  25961  dveflem  25964  dvef  25965  dvferm1  25970  dvferm2  25972  rolle  25975  dvlip  25978  dvlipcn  25979  dv11cn  25986  dvivthlem1  25993  dvivth  25995  lhop1lem  25998  ftc1lem1  26020  ftc1lem5  26025  ftc2  26029  itgsubstlem  26033  tdeglem3  26042  tdeglem4  26043  mdegval  26046  mdegmullem  26061  deg1fval  26063  deg1ldg  26075  deg1leb  26078  coe1mul3  26082  uc1pval  26123  mon1pval  26125  mon1pid  26137  q1pval  26138  r1pval  26141  ply1remlem  26148  ig1pval  26159  plyval  26176  elply2  26179  plyeq0lem  26193  coeval  26206  dgrval  26211  coeid2  26222  coemullem  26233  coemul  26235  elqaalem1  26303  elqaalem2  26304  elqaalem3  26305  iaa  26309  aareccl  26310  aannenlem1  26312  geolim3  26323  aaliou3lem1  26326  aaliou3lem2  26327  aaliou3lem5  26331  aaliou3lem6  26332  aaliou3lem7  26333  aaliou3  26335  tayl0  26345  taylthlem1  26356  taylthlem2  26357  ulmshftlem  26372  ulmshft  26373  ulmuni  26375  ulmcau  26378  ulmdvlem1  26383  ulmdvlem3  26385  mtest  26387  mtestbdd  26388  mbfulm  26389  iblulm  26390  itgulm  26391  pserval  26393  pserval2  26394  radcnvlem1  26396  radcnvlem2  26397  dvradcnv  26404  pserulm  26405  pserdvlem2  26411  pserdv  26412  abelthlem1  26414  abelthlem3  26416  abelthlem4  26417  abelthlem5  26418  abelthlem6  26419  abelthlem7  26421  abelthlem8  26422  abelthlem9  26423  resinf1o  26518  efif1olem4  26527  eff1olem  26530  logcnlem5  26628  logtayllem  26641  logtayl  26642  logtaylsum  26643  logtayl2  26644  logccv  26645  asinval  26864  acosval  26865  atanval  26866  atantayl  26919  leibpilem2  26923  leibpi  26924  leibpisum  26925  log2cnv  26926  log2tlbnd  26927  areaval  26946  efrlim  26951  dfef2  26952  amgmlem  26971  emcllem2  26978  emcllem3  26979  emcllem4  26980  emcllem5  26981  emcllem6  26982  emcllem7  26983  zetacvg  26996  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulm2  27017  lgamcvglem  27021  igamval  27028  lgamcvg2  27036  gamcvg2lem  27040  ftalem7  27060  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  basellem6  27067  basellem8  27069  basellem9  27070  chtval  27091  vmaval  27094  chpval  27103  ppival  27108  muval  27113  prmorcht  27159  sqff1o  27163  dvdsflsumcom  27169  musum  27172  muinv  27174  sgmppw  27178  fsumvma  27194  pclogsum  27196  dchrfi  27236  bposlem5  27269  bposlem7  27271  bposlem8  27272  bposlem9  27273  lgsfval  27283  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  lgsqrlem2  27328  lgsqrlem4  27330  lgseisenlem2  27357  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasumiflem1  27482  dchrvmaeq0  27485  dchrisum0fval  27486  dchrisum0re  27494  mulog2sumlem1  27515  pntrval  27543  pntsval  27553  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntlem3  27590  abvcxp  27596  padicfval  27597  padicval  27598  padicabv  27611  ostth1  27614  ostth2  27618  ostth3  27619  nosupfv  27688  noinffv  27703  newval  27845  leftval  27859  rightval  27860  iscgrg  28598  legval  28670  ishpg  28845  iscgra  28895  isinag  28924  isleag  28933  iseqlg  28953  ttgval  28961  elee  28980  axsegconlem1  29004  axsegconlem9  29012  axsegconlem10  29013  axpasch  29028  axlowdimlem15  29043  axlowdim  29048  axeuclidlem  29049  axcontlem2  29052  eengv  29066  vtxval  29087  iedgval  29088  edgval  29136  vtxdgval  29555  wwlksnextinj  29985  wwlksnextsurj  29986  clwwlkfv  30136  clwwlknonmpo  30177  fusgreg2wsplem  30421  fusgreghash2wsp  30426  numclwwlk1lem2fv  30444  gidval  30601  grpoinvval  30612  bafval  30693  imsval  30774  dipfval  30791  sspval  30812  nmooval  30852  hmoval  30899  ipasslem8  30926  ipasslem9  30927  ipblnfi  30944  ubthlem2  30960  htthlem  31006  normval  31213  ocval  31369  occllem  31392  hsupval  31423  pjhfval  31485  pjhval  31486  chscllem2  31727  chscllem3  31728  hosval  31829  homval  31830  hodval  31831  hfsval  31832  hfmval  31833  brafval  32032  braval  32033  kbval  32043  eigvalval  32049  cnlnadjlem1  32156  nmopadjlei  32177  hmopidmchi  32240  strlem2  32340  hstrlem2  32348  cdj3lem2  32524  ofpreima  32757  psgnfzto1stlem  33181  evpmval  33226  altgnsg  33230  inftmrel  33261  isinftm  33262  qusker  33432  qusvscpbl  33434  qusvsval  33435  mxidlval  33544  idlsrgval  33586  psrmonmul  33734  dimval  33785  dimvalfi  33786  smatfval  33979  lmatval  33997  locfinreflem  34024  rspecval  34048  rmulccn  34112  xrmulc1cn  34114  xrge0iifcv  34118  xrge0iifiso  34119  xrge0iifhom  34121  xrge0iif1  34122  qqhval  34156  rrhval  34180  xrhval  34202  ddeval1  34418  ddeval0  34419  sxbrsigalem0  34455  sxbrsigalem3  34456  eulerpartlemgv  34557  rrvmbfm  34626  dstrvval  34655  coinflippv  34668  ballotlem2  34673  ballotlemfval  34674  ballotlemi  34685  ballotlemsval  34693  ballotlemrval  34702  ballotth  34722  plymulx  34732  signstfv  34747  signsvvfval  34762  onvf1odlem3  35333  derangval  35395  subfacval  35401  erdszelem3  35421  erdszelem9  35427  erdszelem10  35428  txpconn  35460  indispconn  35462  cvxpconn  35470  cvmlift2lem2  35532  cvmlift2lem3  35533  cvmlift2lem7  35537  cvmliftphtlem  35545  cvmlift3lem4  35550  snmlfval  35558  snmlval  35559  gonafv  35578  mvtval  35728  mrsubffval  35735  mrsubcv  35738  mrsubrn  35741  elmrsubrn  35748  msubffval  35751  mvhval  35762  mpstval  35763  mstaval  35772  mclsval  35791  mppsval  35800  sinccvglem  35900  circum  35902  divcnvlin  35961  iprodefisum  35969  iprodgam  35970  faclimlem1  35971  faclimlem2  35972  faclim  35974  iprodfac  35975  faclim2  35976  dfrdg2  36021  findabrcl  36682  dnival  36777  bj-evalval  37433  bj-inftyexpitaudisj  37565  bj-inftyexpiinv  37568  bj-inftyexpidisj  37570  curfv  37967  finixpnum  37972  poimirlem16  38003  poimir  38020  broucube  38021  mblfinlem2  38025  voliunnfl  38031  volsupnfl  38032  itg2addnclem  38038  itg2addnclem3  38040  ftc1cnnc  38059  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anc  38068  ftc2nc  38069  fvopabf4g  38089  sdclem2  38109  fdc  38112  lmclim2  38125  geomcau  38126  istotbnd  38136  isbnd  38147  prdsbnd2  38162  heiborlem6  38183  heiborlem7  38184  heiborlem8  38185  rrnval  38194  rrncmslem  38199  idlval  38380  pridlval  38400  maxidlval  38406  lshpset  39470  lsatset  39482  lcvfbr  39512  lflset  39551  lflnegcl  39567  lshpkrlem1  39602  lshpkrlem2  39603  lshpkrlem3  39604  ldualset  39617  cmtfvalN  39702  cvrfval  39760  pats  39777  llnset  39997  lplnset  40021  lvolset  40064  lineset  40230  pointsetN  40233  psubspset  40236  pmapval  40249  paddfval  40289  pclfvalN  40381  polfvalN  40396  polvalN  40397  psubclsetN  40428  watvalN  40485  lhpset  40487  lautset  40574  pautsetN  40590  ldilset  40601  ltrnset  40610  dilsetN  40645  trnsetN  40648  trlset  40653  trlval  40654  tgrpset  41237  tendoset  41251  tendo02  41279  erngset  41292  erngset-rN  41300  cdlemksv  41336  dvaset  41497  dvaplusgv  41502  diafval  41523  diaval  41524  dvhset  41573  cdlemm10N  41610  docafvalN  41614  djafvalN  41626  dibfval  41633  dibval  41634  dicfval  41667  dicval  41668  dihval  41724  dochfval  41842  djhfval  41889  dochfl1  41968  lpolsetN  41974  lcdval  42081  mapdhval  42216  hvmapfval  42251  hdmap1fval  42288  fimgmcyc  43020  prjspval  43053  isnacs  43153  mzpclval  43174  mzpsubst  43197  mzprename  43198  mzpcompact2lem  43200  eldiophb  43206  diophrw  43208  eldioph2  43211  diophin  43221  diophun  43222  diophren  43258  pell1qrval  43291  pell14qrval  43293  pell1234qrval  43295  pellfundval  43325  rmxypairf1o  43356  rmxyval  43360  mzpcong  43417  pw2f1ocnv  43482  dnnumch1  43489  dfac11  43507  hbtlem1  43568  hbtlem7  43570  elmnc  43581  dgraaval  43589  mpaaval  43596  itgoval  43606  flcidc  43615  mendval  43624  cytpval  43647  cantnfub  43766  cantnfresb  43769  tfsconcatrev  43793  elcnvlem  44045  comptiunov2i  44150  dftrcl3  44164  trclfvcom  44167  cnvtrclfv  44168  cotrcltrcl  44169  trclimalb2  44170  trclfvdecomr  44172  dfrtrcl3  44177  dfrtrcl4  44182  clsk1indlem0  44485  clsk1indlem2  44486  clsk1indlem3  44487  clsk1indlem4  44488  clsk1indlem1  44489  k0004val  44594  lhe4.4ex1a  44773  addrfv  44912  subrfv  44913  mulvfv  44914  monoord2xrv  45926  sumnnodd  46075  liminfgval  46205  ioodvbdlimc2lem  46377  itgsin0pilem1  46393  stoweidlem55  46498  wallispilem1  46508  wallispilem2  46509  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  dirkerval  46534  fourierdlem2  46552  fourierdlem3  46553  fourierdlem29  46579  fourierdlem62  46611  fourierdlem80  46629  fourierdlem103  46652  fourierdlem104  46653  fourierswlem  46673  fouriersw  46674  iundjiunlem  46902  carageniuncllem2  46965  0ome  46972  hoidmv1le  47037  hoidmvlelem3  47040  smflimsuplem7  47269  nthrucw  47331  iccpval  47890  fppr  48217  bigoval  49040  ackval0  49171  ackval41a  49185  eenglngeehlnm  49230  oppcinito  49725  oppctermo  49726  dfinito4  49991  prstcval  50041  mndtcval  50069  setc1onsubc  50092  lmdfval2  50145  cmdfval2  50146  vsetrec  50193  onsetreclem1  50195  elpglem3  50203  pgindnf  50206  sinhval-named  50226  coshval-named  50227  tanhval-named  50228  secval  50237  cscval  50238  cotval  50239  aacllem  50291