Theorem fvmpt 6986

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ↦ cmpt 5186  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541

This theorem is used by:  fvmptex  7001  fvmptrabfv  7019  mptfvmpt  7227  fvmptopab  7468  ofval  7689  caofinvl  7710  fvresex  7957  1stval  7988  2ndval  7989  reldm  8041  curry1val  8102  curry2val  8106  fsplitfpar  8115  fnwelem  8129  brtpos2  8230  onovuni  8331  tz7.44-1  8395  oasuc  8511  oesuclem  8512  omsuc  8513  onasuc  8515  onmsuc  8516  fsetfocdm  8862  curfv  8871  fvmptmap  8888  xpcomco  9065  unxpdomlem1  9226  unfilem2  9276  ordtypelem3  9492  ixpiunwdom  9562  inf3lema  9603  noinfep  9639  cantnfval  9647  cantnflem1d  9667  cantnflem1  9668  ssttrcl  9694  ttrcltr  9695  ttrclselem2  9705  r1sucg  9751  r0weon  10015  infxpenc2lem1  10022  fseqenlem1  10027  fseqenlem2  10028  dfac8alem  10032  ac5num  10039  acni2  10049  dfac4  10125  dfac2a  10132  dfacacn  10144  dfac12lem1  10146  ackbij1lem7  10227  ackbij2lem2  10241  ackbij2lem3  10242  cfsmolem  10272  fin23lem28  10342  fin23lem39  10352  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  fin1a2lem3  10404  itunifval  10418  itunisuc  10421  axdc2lem  10450  axdc3lem2  10453  axcclem  10459  zorn2lem1  10498  negiso  12219  infrenegsup  12222  uzval  12889  flval  13855  ceilval  13899  ceilval2  13901  monoord2  14097  seqf1olem2  14106  seqf1o  14107  seqdistr  14117  serle  14121  seqof  14123  swrdfv  14716  revval  14829  revfv  14832  wwlktovf1  15030  wwlktovfo  15031  sgnval  15161  cjval  15189  reval  15193  imval  15194  sqrtval  15324  absval  15325  limsupval  15561  limsupgval  15563  climmpt  15658  climle  15727  rlimdiv  15733  isercolllem1  15752  isercoll2  15756  caurcvg2  15765  fsumser  15816  isumadd  15853  fsumcnv  15859  fsumrev  15865  fsumshft  15866  iserabs  15902  cvgcmp  15903  cvgcmpce  15905  incexclem  15925  isumless  15934  divcnvshft  15944  supcvg  15945  harmonic  15948  trireciplem  15951  trirecip  15952  expcnv  15953  explecnv  15954  geolim  15959  geolim2  15960  geo2lim  15964  geomulcvg  15965  geoisum  15966  geoisumr  15967  geoisum1  15968  geoisum1c  15969  cvgrat  15972  mertenslem2  15974  mertens  15975  prodfdiv  15985  fprodser  16036  fprodshft  16063  fprodrev  16064  fprodcnv  16070  iprodmul  16090  bpolylem  16134  eftval  16162  efval  16165  efcvgfsum  16172  ege2le3  16176  eftlub  16197  eflegeo  16209  sinval  16210  cosval  16211  tanval  16216  eirrlem  16292  rpnnen2lem1  16302  rpnnen2lem2  16303  bitsfval  16513  bitsinv2  16533  bitsinv  16538  sadcf  16543  sadc0  16544  sadcp1  16545  smupf  16568  smup0  16569  smupp1  16570  qnumval  16828  qdenval  16829  phival  16858  crth  16869  phimullem  16870  eulerthlem2  16873  phisum  16882  odzval  16883  iserodd  16927  pcmpt  16984  prmreclem1  17008  prmreclem2  17009  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  1arithlem1  17015  1arithlem2  17016  vdwapfval  17063  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  vdwlem9  17081  ramub1lem2  17119  ramcl  17121  prmoval  17125  strfvnd  17277  topnval  17519  prdsplusgfval  17559  prdsmulrfval  17561  isacs  17739  acsfn  17747  homffval  17778  comfffval  17786  oppcval  17801  monfval  17821  oppcmon  17827  sectffval  17839  invffval  17847  isoval  17854  idfuval  17965  homafval  18118  arwval  18132  coafval  18153  yonedainv  18369  oduval  18376  pltfval  18417  lubfval  18436  lubval  18442  glbfval  18449  glbval  18455  p0val  18513  p1val  18514  ipoval  18618  plusffval  18736  grpidval  18754  issubmgm  18804  issubm  18911  prdspjmhm  18938  efmnd  18979  smndex1gbas  19011  smndex1gid  19013  smndex1igid  19015  smndex1igidOLD  19016  grpinvfval  19102  grpinvval  19104  grpsubfval  19107  grpsubfvalALT  19108  grplactval  19165  prdsinvlem  19172  mulgfval  19192  mulgfvalALT  19193  pwsmulg  19242  issubg  19249  isnsg  19278  cycsubmel  19328  cycsubgcl  19334  conjghm  19376  conjnmz  19379  cntrval  19446  cntzfval  19447  cntzval  19448  oppgval  19474  psgnfval  19627  psgnval  19634  odfval  19659  odval  19661  sylow1lem4  19728  pgpssslw  19741  sylow2blem3  19749  sylow3lem2  19755  lsmfval  19765  pj1fval  19821  efgval  19844  efgsval  19858  frgpval  19885  vrgpval  19894  mulgmhm  19954  mulgghm  19955  ablfaclem1  20214  mgpval  20276  srglmhm  20360  srgrmhm  20361  ringlghm  20454  ringrghm  20455  pwspjmhmmgpd  20468  pwsexpg  20469  opprval  20479  dvdsrval  20502  isunit  20514  invrfval  20530  dvrfval  20543  isirred  20560  issubrng  20709  issubrg  20733  rgspnval  20774  rrgval  20859  fidomndrnglem  20939  issdrg  20954  abvfval  20976  abvtrivd  20998  staffval  21007  stafval  21008  scaffval  21064  lmodvsghm  21107  lssset  21117  lspfval  21157  islbs  21260  sraval  21359  rlmval  21375  2idlval  21453  lpival  21555  expmhm  21649  expghm  21688  mulgghm2  21689  mulgrhm  21690  zrhval  21720  zrhmulg  21722  zlmval  21728  chrval  21736  znval  21748  znzrhval  21759  evpmss  21799  psgnevpmb  21800  ip0l  21849  ipffval  21861  ocvfval  21879  ocvval  21880  cssval  21895  thlval  21908  pjfval  21919  pjval  21923  isobs  21933  prdsinvgd2  21955  uvcresum  22006  frlmup1  22011  frlmup2  22012  islinds  22022  islindf5  22052  aspval  22087  asclval  22094  psrmulval  22159  psrlidm  22176  psrridm  22177  psrascl  22193  mvrval  22196  mvrval2  22197  mplmonmul  22252  evlslem3  22296  evlslem1  22298  evlsval  22302  evlssca  22310  evlsvar  22311  psdmul  22394  psdmvr  22397  psr1val  22411  vr1val  22417  ply1val  22419  coe1fval  22430  coe1fv  22431  coe1tmmul2  22502  coe1tmmul  22503  coe1tmmul2fv  22504  coe1pwmulfv  22506  evls1val  22545  evl1fval  22553  evl1val  22554  mamulid  22663  mamurid  22664  mdetleib  22809  mdetleib1  22813  mdetunilem9  22842  mdetuni0  22843  mdetmul  22845  cpmidpmatlem1  23095  ordtval  23414  cnpval  23461  ptpjpre1  23797  ptpjopn  23838  dfac14  23844  upxp  23849  uptx  23851  hauseqlcld  23872  txlm  23874  xkoptsub  23880  xkoinjcn  23913  kqval  23952  xpstopnlem1  24035  fmval  24169  flfval  24216  ptcmplem2  24279  ptcmplem3  24280  symgtgp  24332  qustgpopn  24346  ussval  24485  iscfilu  24513  ispsmet  24530  ismet  24549  isxmet  24550  mopnval  24664  prdsxmslem2  24755  nmfval  24814  nmval  24815  nmoval  24941  metdsval  25074  divcn  25096  mulc1cncf  25133  icopnfhmeo  25171  iccpnfhmeo  25173  xrhmeo  25174  cnheiborlem  25182  evth  25187  evth2  25188  lebnumlem3  25191  isphtpy  25209  isphtpc  25222  pcofval  25238  pcovalg  25240  pco1  25243  pcopt  25250  pcopt2  25251  pcoass  25252  pcorevcl  25253  pcorevlem  25254  pcorev2  25256  pi1xfrcnv  25285  cphnm  25421  tcphval  25446  tcphnmval  25457  cfilfval  25492  iscmet  25512  iscmet3lem3  25518  rrxval  25615  ehlval  25642  ivth2  25683  ovolval  25701  ovollb2lem  25716  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliunlem2  25731  ovolicc1  25744  voliunlem1  25778  voliunlem2  25779  voliunlem3  25780  volsup  25784  ioorval  25802  uniioombllem3  25813  uniioombllem6  25816  volsup2  25833  volcn  25834  volivth  25835  vitalilem2  25837  vitalilem3  25838  vitalilem4  25839  vitali  25841  mbfmax  25877  mbfimaopnlem  25883  itg1val  25911  i1f1lem  25917  itg11  25919  itg1addlem4  25927  itg1mulc  25932  i1fres  25933  itg1climres  25942  mbfi1fseqlem2  25944  mbfi1fseqlem3  25945  mbfi1fseqlem6  25948  mbfi1flimlem  25950  mbfi1flim  25951  mbfmullem2  25952  itg2seq  25970  itg2uba  25971  itg2splitlem  25976  itg2monolem1  25978  itg2monolem2  25979  itg2monolem3  25980  itg2mono  25981  itg2i1fseqle  25982  itg2i1fseq  25983  itg2i1fseq2  25984  itg2addlem  25986  itg2cnlem1  25989  itg2cn  25991  limccnp2  26119  dvnff  26150  dvnp1  26152  cpnfval  26159  elcpn  26161  dvrec  26182  dvcnvlem  26203  dveflem  26206  dvef  26207  dvferm1  26212  dvferm2  26214  rolle  26217  dvlip  26220  dvlipcn  26221  dv11cn  26228  dvivthlem1  26235  dvivth  26237  lhop1lem  26240  ftc1lem1  26262  ftc1lem5  26267  ftc2  26271  itgsubstlem  26275  tdeglem3  26284  tdeglem4  26285  mdegval  26288  mdegmullem  26303  deg1fval  26305  deg1ldg  26317  deg1leb  26320  coe1mul3  26324  uc1pval  26365  mon1pval  26367  mon1pid  26379  q1pval  26380  r1pval  26383  ply1remlem  26390  ig1pval  26401  plyval  26418  elply2  26421  plyeq0lem  26436  coeval  26449  dgrval  26454  coeid2  26465  coemullem  26476  coemul  26478  plymulidp  26512  elqaalem1  26551  elqaalem2  26552  elqaalem3  26553  iaa  26560  iaaOLD  26561  aareccl  26562  aannenlem1  26564  geolim3  26575  aaliou3lem1  26578  aaliou3lem2  26579  aaliou3lem5  26583  aaliou3lem6  26584  aaliou3lem7  26585  aaliou3  26587  aaliou3r  26588  tayl0  26598  taylthlem1  26609  taylthlem2  26610  ulmshftlem  26625  ulmshft  26626  ulmuni  26628  ulmcau  26631  ulmdvlem1  26636  ulmdvlem3  26638  mtest  26640  mtestbdd  26641  mbfulm  26642  iblulm  26643  itgulm  26644  pserval  26646  pserval2  26647  radcnvlem1  26649  radcnvlem2  26650  dvradcnv  26657  pserulm  26658  pserdvlem2  26664  pserdv  26665  abelthlem1  26667  abelthlem3  26669  abelthlem4  26670  abelthlem5  26671  abelthlem6  26672  abelthlem7  26674  abelthlem8  26675  abelthlem9  26676  resinf1o  26773  efif1olem4  26782  eff1olem  26785  logcnlem5  26883  logtayllem  26896  logtayl  26897  logtaylsum  26898  logtayl2  26899  logccv  26900  asinval  27119  acosval  27120  atanval  27121  atantayl  27174  leibpilem2  27178  leibpi  27179  leibpisum  27180  log2cnv  27181  log2tlbnd  27182  areaval  27201  efrlim  27206  dfef2  27207  amgmlem  27226  emcllem2  27233  emcllem3  27234  emcllem4  27235  emcllem5  27236  emcllem6  27237  emcllem7  27238  zetacvg  27251  lgamgulmlem4  27268  lgamgulmlem5  27269  lgamgulm2  27272  lgamcvglem  27276  igamval  27283  lgamcvg2  27291  gamcvg2lem  27295  ftalem7  27315  basellem2  27318  basellem3  27319  basellem4  27320  basellem5  27321  basellem6  27322  basellem8  27324  basellem9  27325  chtval  27346  vmaval  27349  chpval  27358  ppival  27363  muval  27368  prmorcht  27414  sqff1o  27418  dvdsflsumcom  27424  musum  27427  muinv  27429  sgmppw  27433  fsumvma  27449  pclogsum  27451  dchrfi  27491  bposlem5  27524  bposlem7  27526  bposlem8  27527  bposlem9  27528  lgsfval  27538  lgsdir  27568  lgsdilem2  27569  lgsdi  27570  lgsne0  27571  lgsqrlem2  27583  lgsqrlem4  27585  lgseisenlem2  27612  dchrmusum2  27730  dchrvmasumlem1  27731  dchrvmasumiflem1  27737  dchrvmaeq0  27740  dchrisum0fval  27741  dchrisum0re  27749  mulog2sumlem1  27770  pntrval  27798  pntsval  27808  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntlem3  27845  abvcxp  27851  padicfval  27852  padicval  27853  padicabv  27866  ostth1  27869  ostth2  27873  ostth3  27874  nosupfv  27942  noinffv  27957  newval  28100  leftval  28114  rightval  28115  iscgrg  28854  legval  28926  ishpg  29116  iscgra  29195  isinag  29236  isleag  29245  iseqlg  29291  ttgval  29331  elee  29350  axsegconlem1  29374  axsegconlem9  29382  axsegconlem10  29383  axpasch  29398  axlowdimlem15  29413  axlowdim  29418  axeuclidlem  29419  axcontlem2  29422  eengv  29436  vtxval  29457  iedgval  29458  edgval  29506  vtxdgval  29928  wwlksnextinj  30367  wwlksnextsurj  30368  clwwlkfv  30518  clwwlknonmpo  30559  fusgreg2wsplem  30813  fusgreghash2wsp  30818  numclwwlk1lem2fv  30836  gidval  30993  grpoinvval  31004  bafval  31085  imsval  31166  dipfval  31183  sspval  31204  nmooval  31244  hmoval  31291  ipasslem8  31318  ipasslem9  31319  ipblnfi  31336  ubthlem2  31352  htthlem  31398  normval  31605  ocval  31761  occllem  31784  hsupval  31815  pjhfval  31877  pjhval  31878  chscllem2  32119  chscllem3  32120  hosval  32221  homval  32222  hodval  32223  hfsval  32224  hfmval  32225  brafval  32424  braval  32425  kbval  32435  eigvalval  32441  cnlnadjlem1  32548  nmopadjlei  32569  hmopidmchi  32632  strlem2  32732  hstrlem2  32740  cdj3lem2  32916  ofpreima  33138  psgnfzto1stlem  33540  evpmval  33585  altgnsg  33589  inftmrel  33620  isinftm  33621  qusker  33789  qusvscpbl  33791  qusvsval  33792  mxidlval  33864  idlsrgval  33913  psrmonmul  34060  dimval  34111  dimvalfi  34112  smatfval  34305  lmatval  34323  locfinreflem  34350  rspecval  34374  rmulccn  34438  xrmulc1cn  34440  xrge0iifcv  34444  xrge0iifiso  34445  xrge0iifhom  34447  xrge0iif1  34448  qqhval  34482  rrhval  34506  xrhval  34528  ddeval1  34745  ddeval0  34746  sxbrsigalem0  34782  sxbrsigalem3  34783  eulerpartlemgv  34884  rrvmbfm  34953  dstrvval  34982  coinflippv  34995  ballotlem2  35000  ballotlemfval  35001  ballotlemi  35012  ballotlemsval  35020  ballotlemrval  35029  ballotth  35049  signstfv  35071  signsvvfval  35086  kardval  35678  kard0  35680  onvf1odlem3  35702  derangval  35746  subfacval  35752  erdszelem3  35772  erdszelem9  35778  erdszelem10  35779  txpconn  35811  indispconn  35813  cvxpconn  35821  cvmlift2lem2  35883  cvmlift2lem3  35884  cvmlift2lem7  35888  cvmliftphtlem  35896  cvmlift3lem4  35901  snmlfval  35909  snmlval  35910  gonafv  35929  mvtval  36079  mrsubffval  36086  mrsubcv  36089  mrsubrn  36092  elmrsubrn  36099  msubffval  36102  mvhval  36113  mpstval  36114  mstaval  36123  mclsval  36142  mppsval  36151  sinccvglem  36251  circum  36253  divcnvlin  36312  iprodefisum  36320  iprodgam  36321  faclimlem1  36322  faclimlem2  36323  faclim  36325  iprodfac  36326  faclim2  36327  dfrdg2  36372  findabrcl  37073  dnival  37168  bj-evalval  37825  bj-inftyexpitaudisj  37957  bj-inftyexpiinv  37960  bj-inftyexpidisj  37962  finixpnum  38359  poimirlem16  38385  poimir  38402  broucube  38403  mblfinlem2  38407  voliunnfl  38413  volsupnfl  38414  itg2addnclem  38420  itg2addnclem3  38422  ftc1cnnc  38441  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anc  38450  ftc2nc  38451  fvopabf4g  38472  sdclem2  38492  fdc  38495  lmclim2  38508  geomcau  38509  istotbnd  38519  isbnd  38530  prdsbnd2  38545  heiborlem6  38566  heiborlem7  38567  heiborlem8  38568  rrnval  38577  rrncmslem  38582  idlval  38763  pridlval  38783  maxidlval  38789  lshpset  39851  lsatset  39863  lcvfbr  39893  lflset  39932  lflnegcl  39948  lshpkrlem1  39983  lshpkrlem2  39984  lshpkrlem3  39985  ldualset  39998  cmtfvalN  40083  cvrfval  40141  pats  40158  llnset  40378  lplnset  40402  lvolset  40445  lineset  40611  pointsetN  40614  psubspset  40617  pmapval  40630  paddfval  40670  pclfvalN  40762  polfvalN  40777  polvalN  40778  psubclsetN  40809  watvalN  40866  lhpset  40868  lautset  40955  pautsetN  40971  ldilset  40982  ltrnset  40991  dilsetN  41026  trnsetN  41029  trlset  41034  trlval  41035  tgrpset  41618  tendoset  41632  tendo02  41660  erngset  41673  erngset-rN  41681  cdlemksv  41717  dvaset  41878  dvaplusgv  41883  diafval  41904  diaval  41905  dvhset  41954  cdlemm10N  41991  docafvalN  41995  djafvalN  42007  dibfval  42014  dibval  42015  dicfval  42048  dicval  42049  dihval  42105  dochfval  42223  djhfval  42270  dochfl1  42349  lpolsetN  42355  lcdval  42462  mapdhval  42597  hvmapfval  42632  hdmap1fval  42669  fimgmcyc  43416  prjspval  43449  isnacs  43549  mzpclval  43570  mzpsubst  43593  mzprename  43594  mzpcompact2lem  43596  eldiophb  43602  diophrw  43604  eldioph2  43607  diophin  43617  diophun  43618  diophren  43654  pell1qrval  43687  pell14qrval  43689  pell1234qrval  43691  pellfundval  43721  rmxypairf1o  43752  rmxyval  43756  mzpcong  43813  pw2f1ocnv  43878  dnnumch1  43885  dfac11  43903  hbtlem1  43964  hbtlem7  43966  elmnc  43977  dgraaval  43985  mpaaval  43992  itgoval  44002  flcidc  44011  mendval  44020  cytpval  44043  cantnfub  44162  cantnfresb  44165  tfsconcatrev  44189  elcnvlem  44441  comptiunov2i  44546  dftrcl3  44560  trclfvcom  44563  cnvtrclfv  44564  cotrcltrcl  44565  trclimalb2  44566  trclfvdecomr  44568  dfrtrcl3  44573  dfrtrcl4  44578  clsk1indlem0  44881  clsk1indlem2  44882  clsk1indlem3  44883  clsk1indlem4  44884  clsk1indlem1  44885  k0004val  44990  lhe4.4ex1a  45153  addrfv  45291  subrfv  45292  mulvfv  45293  monoord2xrv  46311  sumnnodd  46460  liminfgval  46590  ioodvbdlimc2lem  46762  itgsin0pilem1  46778  stoweidlem55  46883  wallispilem1  46893  wallispilem2  46894  wallispilem4  46896  wallispi2lem1  46899  wallispi2lem2  46900  dirkerval  46919  fourierdlem2  46937  fourierdlem3  46938  fourierdlem29  46964  fourierdlem62  46996  fourierdlem80  47014  fourierdlem103  47037  fourierdlem104  47038  fourierswlem  47058  fouriersw  47059  iundjiunlem  47287  carageniuncllem2  47350  0ome  47357  hoidmv1le  47422  hoidmvlelem3  47425  smflimsuplem7  47654  sqrtnnaa  47731  sqrtnzqaa  47732  sqrtnpoly  47761  iccpval  48315  fppr  48642  bigoval  49479  ackval0  49610  ackval41a  49624  eenglngeehlnm  49669  oppcinito  50161  oppctermo  50162  dfinito4  50427  prstcval  50477  mndtcval  50505  setc1onsubc  50528  lmdfval2  50581  cmdfval2  50582  vsetrec  50629  onsetreclem1  50631  elpglem3  50639  pgindnf  50642  sinhval-named  50662  coshval-named  50663  tanhval-named  50664  secval  50673  cscval  50674  cotval  50675  aacllem  50772