Theorem fvmpt 6998

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fv 6551

This theorem is used by:  fvmptex  7013  fvmptrabfv  7031  mptfvmpt  7238  fvmptopab  7479  ofval  7708  caofinvl  7729  fvresex  7976  1stval  8007  2ndval  8008  reldm  8059  curry1val  8122  curry2val  8126  fsplitfpar  8135  fnwelem  8149  brtpos2  8256  onovuni  8357  tz7.44-1  8421  oasuc  8539  oesuclem  8540  omsuc  8541  onasuc  8543  onmsuc  8544  fsetfocdm  8890  curfv  8899  fvmptmap  8916  xpcomco  9093  unxpdomlem1  9254  unfilem2  9305  ordtypelem3  9521  ixpiunwdom  9591  inf3lema  9632  noinfep  9668  cantnfval  9676  cantnflem1d  9696  cantnflem1  9697  ssttrcl  9723  ttrcltr  9724  ttrclselem2  9734  r1sucg  9783  r0weon  10098  infxpenc2lem1  10105  fseqenlem1  10110  fseqenlem2  10111  dfac8alem  10115  ac5num  10122  acni2  10132  dfac4  10208  dfac2a  10215  dfacacn  10227  dfac12lem1  10229  ackbij1lem7  10310  ackbij2lem2  10324  ackbij2lem3  10325  cfsmolem  10355  fin23lem28  10425  fin23lem39  10435  isf32lem6  10443  isf32lem7  10444  isf32lem8  10445  fin1a2lem3  10487  itunifval  10501  itunisuc  10504  axdc2lem  10533  axdc3lem2  10536  axcclem  10542  zorn2lem1  10581  negiso  12304  infrenegsup  12307  uzval  12974  flval  13941  ceilval  13985  ceilval2  13987  monoord2  14183  seqf1olem2  14192  seqf1o  14193  seqdistr  14203  serle  14207  seqof  14209  swrdfv  14804  revval  14917  revfv  14920  wwlktovf1  15119  wwlktovfo  15120  sgnval  15250  cjval  15278  reval  15282  imval  15283  sqrtval  15413  absval  15414  limsupval  15650  limsupgval  15652  climmpt  15747  climle  15816  rlimdiv  15822  isercolllem1  15841  isercoll2  15845  caurcvg2  15854  fsumser  15905  isumadd  15942  fsumcnv  15948  fsumrev  15954  fsumshft  15955  iserabs  15991  cvgcmp  15992  cvgcmpce  15994  incexclem  16014  isumless  16023  divcnvshft  16033  supcvg  16034  harmonic  16037  trireciplem  16040  trirecip  16041  expcnv  16042  explecnv  16043  geolim  16048  geolim2  16049  geo2lim  16053  geomulcvg  16054  geoisum  16055  geoisumr  16056  geoisum1  16057  geoisum1c  16058  cvgrat  16061  mertenslem2  16063  mertens  16064  prodfdiv  16074  fprodser  16125  fprodshft  16152  fprodrev  16153  fprodcnv  16159  iprodmul  16179  bpolylem  16223  eftval  16251  efval  16254  efcvgfsum  16261  ege2le3  16265  eftlub  16286  eflegeo  16298  sinval  16299  cosval  16300  tanval  16305  eirrlem  16381  rpnnen2lem1  16391  rpnnen2lem2  16392  bitsfval  16602  bitsinv2  16622  bitsinv  16627  sadcf  16632  sadc0  16633  sadcp1  16634  smupf  16657  smup0  16658  smupp1  16659  qnumval  16922  qdenval  16923  phival  16953  crth  16964  phimullem  16965  eulerthlem2  16968  phisum  16977  odzval  16978  iserodd  17022  pcmpt  17079  prmreclem1  17103  prmreclem2  17104  prmreclem4  17106  prmreclem5  17107  prmreclem6  17108  1arithlem1  17110  1arithlem2  17111  vdwapfval  17158  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  vdwlem9  17176  ramub1lem2  17214  ramcl  17216  prmoval  17220  strfvnd  17372  topnval  17614  prdsplusgfval  17654  prdsmulrfval  17656  isacs  17834  acsfn  17842  homffval  17873  comfffval  17881  oppcval  17896  monfval  17916  oppcmon  17922  sectffval  17934  invffval  17942  isoval  17949  idfuval  18060  homafval  18213  arwval  18227  coafval  18248  yonedainv  18464  oduval  18471  pltfval  18512  lubfval  18531  lubval  18537  glbfval  18544  glbval  18550  p0val  18608  p1val  18609  ipoval  18713  plusffval  18831  grpidval  18849  issubmgm  18900  issubm  19007  prdspjmhm  19034  efmnd  19075  smndex1gbas  19107  smndex1gid  19109  smndex1igid  19111  smndex1igidOLD  19112  grpinvfval  19198  grpinvval  19200  grpsubfval  19203  grpsubfvalALT  19204  grplactval  19261  prdsinvlem  19268  mulgfval  19288  mulgfvalALT  19289  pwsmulg  19338  issubg  19345  isnsg  19374  cycsubmel  19424  cycsubgcl  19430  conjghm  19472  conjnmz  19475  cntrval  19542  cntzfval  19543  cntzval  19544  oppgval  19570  psgnfval  19723  psgnval  19730  odfval  19755  odval  19757  sylow1lem4  19824  pgpssslw  19837  sylow2blem3  19845  sylow3lem2  19851  lsmfval  19861  pj1fval  19917  efgval  19940  efgsval  19954  frgpval  19981  vrgpval  19990  mulgmhm  20050  mulgghm  20051  ablfaclem1  20310  mgpval  20372  srglmhm  20456  srgrmhm  20457  ringlghm  20552  ringrghm  20553  pwspjmhmmgpd  20566  pwsexpg  20567  opprval  20577  dvdsrval  20600  isunit  20612  invrfval  20628  dvrfval  20641  isirred  20658  issubrng  20808  issubrg  20832  rgspnval  20873  rrgval  20958  fidomndrnglem  21039  issdrg  21054  abvfval  21076  abvtrivd  21098  staffval  21107  stafval  21108  scaffval  21164  lmodvsghm  21207  lssset  21217  lspfval  21257  islbs  21360  sraval  21459  rlmval  21475  2idlval  21553  lpival  21657  expmhm  21751  expghm  21790  mulgghm2  21791  mulgrhm  21792  zrhval  21822  zrhmulg  21824  zlmval  21830  chrval  21838  znval  21850  znzrhval  21861  evpmss  21901  psgnevpmb  21902  ip0l  21951  ipffval  21963  ocvfval  21981  ocvval  21982  cssval  21997  thlval  22010  pjfval  22021  pjval  22025  isobs  22035  prdsinvgd2  22057  uvcresum  22108  frlmup1  22113  frlmup2  22114  islinds  22124  islindf5  22154  aspval  22189  asclval  22196  psrmulval  22261  psrlidm  22278  psrridm  22279  psrascl  22295  mvrval  22298  mvrval2  22299  mplmonmul  22354  evlslem3  22398  evlslem1  22400  evlsval  22404  evlssca  22412  evlsvar  22413  psdmul  22496  psdmvr  22499  psr1val  22513  vr1val  22519  ply1val  22521  coe1fval  22532  coe1fv  22533  coe1tmmul2  22604  coe1tmmul  22605  coe1tmmul2fv  22606  coe1pwmulfv  22608  evls1val  22647  evl1fval  22655  evl1val  22656  mamulid  22765  mamurid  22766  mdetleib  22911  mdetleib1  22915  mdetunilem9  22944  mdetuni0  22945  mdetmul  22947  cpmidpmatlem1  23197  ordtval  23516  cnpval  23563  ptpjpre1  23899  ptpjopn  23940  dfac14  23946  upxp  23951  uptx  23953  hauseqlcld  23974  txlm  23976  xkoptsub  23982  xkoinjcn  24015  kqval  24054  xpstopnlem1  24137  fmval  24271  flfval  24318  ptcmplem2  24381  ptcmplem3  24382  symgtgp  24434  qustgpopn  24448  ussval  24587  iscfilu  24615  ispsmet  24632  ismet  24651  isxmet  24652  mopnval  24766  prdsxmslem2  24857  nmfval  24916  nmval  24917  nmoval  25043  metdsval  25176  divcn  25198  mulc1cncf  25235  icopnfhmeo  25273  iccpnfhmeo  25275  xrhmeo  25276  cnheiborlem  25284  evth  25289  evth2  25290  lebnumlem3  25293  isphtpy  25311  isphtpc  25324  pcofval  25340  pcovalg  25342  pco1  25345  pcopt  25352  pcopt2  25353  pcoass  25354  pcorevcl  25355  pcorevlem  25356  pcorev2  25358  pi1xfrcnv  25387  cphnm  25523  tcphval  25548  tcphnmval  25559  cfilfval  25594  iscmet  25614  iscmet3lem3  25620  rrxval  25717  ehlval  25744  ivth2  25785  ovolval  25803  ovollb2lem  25818  ovolunlem1a  25826  ovolunlem1  25827  ovoliunlem1  25832  ovoliunlem2  25833  ovolicc1  25846  voliunlem1  25880  voliunlem2  25881  voliunlem3  25882  volsup  25886  ioorval  25904  uniioombllem3  25915  uniioombllem6  25918  volsup2  25935  volcn  25936  volivth  25937  vitalilem2  25939  vitalilem3  25940  vitalilem4  25941  vitali  25943  mbfmax  25979  mbfimaopnlem  25985  itg1val  26013  i1f1lem  26019  itg11  26021  itg1addlem4  26029  itg1mulc  26034  i1fres  26035  itg1climres  26044  mbfi1fseqlem2  26046  mbfi1fseqlem3  26047  mbfi1fseqlem6  26050  mbfi1flimlem  26052  mbfi1flim  26053  mbfmullem2  26054  itg2seq  26072  itg2uba  26073  itg2splitlem  26078  itg2monolem1  26080  itg2monolem2  26081  itg2monolem3  26082  itg2mono  26083  itg2i1fseqle  26084  itg2i1fseq  26085  itg2i1fseq2  26086  itg2addlem  26088  itg2cnlem1  26091  itg2cn  26093  limccnp2  26221  dvnff  26252  dvnp1  26254  cpnfval  26261  elcpn  26263  dvrec  26284  dvcnvlem  26305  dveflem  26308  dvef  26309  dvferm1  26314  dvferm2  26316  rolle  26319  dvlip  26322  dvlipcn  26323  dv11cn  26330  dvivthlem1  26337  dvivth  26339  lhop1lem  26342  ftc1lem1  26364  ftc1lem5  26369  ftc2  26373  itgsubstlem  26377  tdeglem3  26386  tdeglem4  26387  mdegval  26390  mdegmullem  26405  deg1fval  26407  deg1ldg  26419  deg1leb  26422  coe1mul3  26426  uc1pval  26467  mon1pval  26469  mon1pid  26481  q1pval  26482  r1pval  26485  ply1remlem  26492  ig1pval  26503  plyval  26520  elply2  26523  plyeq0lem  26538  coeval  26551  dgrval  26556  coeid2  26567  coemullem  26578  coemul  26580  plymulidp  26612  elqaalem1  26651  elqaalem2  26652  elqaalem3  26653  iaa  26660  iaaOLD  26661  aareccl  26662  aannenlem1  26664  geolim3  26675  aaliou3lem1  26678  aaliou3lem2  26679  aaliou3lem5  26683  aaliou3lem6  26684  aaliou3lem7  26685  aaliou3  26687  aaliou3r  26688  tayl0  26698  taylthlem1  26709  taylthlem2  26710  ulmshftlem  26725  ulmshft  26726  ulmuni  26728  ulmcau  26731  ulmdvlem1  26736  ulmdvlem3  26738  mtest  26740  mtestbdd  26741  mbfulm  26742  iblulm  26743  itgulm  26744  pserval  26746  pserval2  26747  radcnvlem1  26749  radcnvlem2  26750  dvradcnv  26757  pserulm  26758  pserdvlem2  26764  pserdv  26765  abelthlem1  26767  abelthlem3  26769  abelthlem4  26770  abelthlem5  26771  abelthlem6  26772  abelthlem7  26774  abelthlem8  26775  abelthlem9  26776  resinf1o  26873  efif1olem4  26882  eff1olem  26885  logcnlem5  26983  logtayllem  26996  logtayl  26997  logtaylsum  26998  logtayl2  26999  logccv  27000  asinval  27219  acosval  27220  atanval  27221  atantayl  27274  leibpilem2  27278  leibpi  27279  leibpisum  27280  log2cnv  27281  log2tlbnd  27282  areaval  27301  efrlim  27306  dfef2  27307  amgmlem  27326  emcllem2  27333  emcllem3  27334  emcllem4  27335  emcllem5  27336  emcllem6  27337  emcllem7  27338  zetacvg  27351  lgamgulmlem4  27368  lgamgulmlem5  27369  lgamgulm2  27372  lgamcvglem  27376  igamval  27383  lgamcvg2  27391  gamcvg2lem  27395  ftalem7  27415  basellem2  27418  basellem3  27419  basellem4  27420  basellem5  27421  basellem6  27422  basellem8  27424  basellem9  27425  chtval  27446  vmaval  27449  chpval  27458  ppival  27463  muval  27468  prmorcht  27514  sqff1o  27518  dvdsflsumcom  27524  musum  27527  muinv  27529  sgmppw  27533  fsumvma  27549  pclogsum  27551  dchrfi  27591  bposlem5  27624  bposlem7  27626  bposlem8  27627  bposlem9  27628  lgsfval  27638  lgsdir  27668  lgsdilem2  27669  lgsdi  27670  lgsne0  27671  lgsqrlem2  27683  lgsqrlem4  27685  lgseisenlem2  27712  dchrmusum2  27830  dchrvmasumlem1  27831  dchrvmasumiflem1  27837  dchrvmaeq0  27840  dchrisum0fval  27841  dchrisum0re  27849  mulog2sumlem1  27870  pntrval  27898  pntsval  27908  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntlem3  27945  abvcxp  27951  padicfval  27952  padicval  27953  padicabv  27966  ostth1  27969  ostth2  27973  ostth3  27974  nosupfv  28072  noinffv  28087  newval  28230  leftval  28244  rightval  28245  iscgrg  28984  legval  29056  ishpg  29246  iscgra  29325  isinag  29366  isleag  29375  iseqlg  29421  ttgval  29461  elee  29480  axsegconlem1  29504  axsegconlem9  29512  axsegconlem10  29513  axpasch  29528  axlowdimlem15  29543  axlowdim  29548  axeuclidlem  29549  axcontlem2  29552  eengv  29566  vtxval  29587  iedgval  29588  edgval  29636  vtxdgval  30058  wwlksnextinj  30497  wwlksnextsurj  30498  clwwlkfv  30648  clwwlknonmpo  30689  fusgreg2wsplem  30943  fusgreghash2wsp  30948  numclwwlk1lem2fv  30966  gidval  31123  grpoinvval  31134  bafval  31215  imsval  31296  dipfval  31313  sspval  31334  nmooval  31374  hmoval  31421  ipasslem8  31448  ipasslem9  31449  ipblnfi  31466  ubthlem2  31482  htthlem  31528  normval  31735  ocval  31891  occllem  31914  hsupval  31945  pjhfval  32007  pjhval  32008  chscllem2  32249  chscllem3  32250  hosval  32351  homval  32352  hodval  32353  hfsval  32354  hfmval  32355  brafval  32554  braval  32555  kbval  32565  eigvalval  32571  cnlnadjlem1  32678  nmopadjlei  32699  hmopidmchi  32762  strlem2  32862  hstrlem2  32870  cdj3lem2  33046  ofpreima  33310  psgnfzto1stlem  33711  evpmval  33756  altgnsg  33760  inftmrel  33791  isinftm  33792  qusker  33960  qusvscpbl  33962  qusvsval  33963  mxidlval  34036  idlsrgval  34085  psrmonmul  34232  dimval  34283  dimvalfi  34284  smatfval  34477  lmatval  34495  locfinreflem  34522  rspecval  34546  rmulccn  34610  xrmulc1cn  34612  xrge0iifcv  34616  xrge0iifiso  34617  xrge0iifhom  34619  xrge0iif1  34620  qqhval  34654  rrhval  34678  xrhval  34700  ddeval1  34917  ddeval0  34918  sxbrsigalem0  34953  sxbrsigalem3  34954  eulerpartlemgv  35055  rrvmbfm  35124  dstrvval  35153  coinflippv  35166  ballotlem2  35171  ballotlemfval  35172  ballotlemi  35183  ballotlemsval  35191  ballotlemrval  35200  ballotth  35220  signstfv  35242  signsvvfval  35257  kardval  35880  kard0  35882  j00smo  35948  maxssj0  35949  onvf1odlem3  35956  derangval  36022  subfacval  36028  erdszelem3  36048  erdszelem9  36054  erdszelem10  36055  txpconn  36087  indispconn  36089  cvxpconn  36097  cvmlift2lem2  36159  cvmlift2lem3  36160  cvmlift2lem7  36164  cvmliftphtlem  36172  cvmlift3lem4  36177  snmlfval  36185  snmlval  36186  gonafv  36205  mvtval  36355  mrsubffval  36362  mrsubcv  36365  mrsubrn  36368  elmrsubrn  36375  msubffval  36378  mvhval  36389  mpstval  36390  mstaval  36399  mclsval  36418  mppsval  36427  sinccvglem  36527  circum  36529  mirimanoffr  36550  divcnvlin  36594  iprodefisum  36602  iprodgam  36603  faclimlem1  36604  faclimlem2  36605  faclim  36607  iprodfac  36608  faclim2  36609  dfrdg2  36653  findabrcl  37338  dnival  37433  bj-evalval  38104  bj-inftyexpitaudisj  38235  bj-inftyexpiinv  38238  bj-inftyexpidisj  38240  finixpnum  38637  poimirlem16  38663  poimir  38680  broucube  38681  mblfinlem2  38685  voliunnfl  38691  volsupnfl  38692  itg2addnclem  38698  itg2addnclem3  38700  ftc1cnnc  38719  ftc1anclem5  38724  ftc1anclem6  38725  ftc1anclem7  38726  ftc1anc  38728  ftc2nc  38729  varprop  38751  negprop  38752  impprop  38753  dfprop2  38755  fvopabf4g  38765  sdclem2  38785  fdc  38788  lmclim2  38801  geomcau  38802  istotbnd  38812  isbnd  38823  prdsbnd2  38838  heiborlem6  38859  heiborlem7  38860  heiborlem8  38861  rrnval  38870  rrncmslem  38875  idlval  39056  pridlval  39076  maxidlval  39082  lshpset  40144  lsatset  40156  lcvfbr  40186  lflset  40225  lflnegcl  40241  lshpkrlem1  40276  lshpkrlem2  40277  lshpkrlem3  40278  ldualset  40291  cmtfvalN  40376  cvrfval  40434  pats  40451  llnset  40671  lplnset  40695  lvolset  40738  lineset  40904  pointsetN  40907  psubspset  40910  pmapval  40923  paddfval  40963  pclfvalN  41055  polfvalN  41070  polvalN  41071  psubclsetN  41102  watvalN  41159  lhpset  41161  lautset  41248  pautsetN  41264  ldilset  41275  ltrnset  41284  dilsetN  41319  trnsetN  41322  trlset  41327  trlval  41328  tgrpset  41911  tendoset  41925  tendo02  41953  erngset  41966  erngset-rN  41974  cdlemksv  42010  dvaset  42171  dvaplusgv  42176  diafval  42197  diaval  42198  dvhset  42247  cdlemm10N  42284  docafvalN  42288  djafvalN  42300  dibfval  42307  dibval  42308  dicfval  42341  dicval  42342  dihval  42398  dochfval  42516  djhfval  42563  dochfl1  42642  lpolsetN  42648  lcdval  42755  mapdhval  42890  hvmapfval  42925  hdmap1fval  42962  fimgmcyc  43707  prjspval  43740  isnacs  43824  mzpclval  43845  mzpsubst  43868  mzprename  43869  mzpcompact2lem  43871  eldiophb  43877  diophrw  43879  eldioph2  43882  diophin  43892  diophun  43893  diophren  43929  pell1qrval  43962  pell14qrval  43964  pell1234qrval  43966  pellfundval  43996  rmxypairf1o  44027  rmxyval  44031  mzpcong  44088  pw2f1ocnv  44153  dnnumch1  44160  dfac11  44173  hbtlem1  44234  hbtlem7  44236  elmnc  44247  dgraaval  44255  mpaaval  44262  itgoval  44272  flcidc  44281  mendval  44290  cytpval  44313  cantnfub  44432  cantnfresb  44435  tfsconcatrev  44459  elcnvlem  44710  comptiunov2i  44815  dftrcl3  44829  trclfvcom  44832  cnvtrclfv  44833  cotrcltrcl  44834  trclimalb2  44835  trclfvdecomr  44837  dfrtrcl3  44842  dfrtrcl4  44847  clsk1indlem0  45150  clsk1indlem2  45151  clsk1indlem3  45152  clsk1indlem4  45153  clsk1indlem1  45154  k0004val  45259  lhe4.4ex1a  45422  addrfv  45559  subrfv  45560  mulvfv  45561  monoord2xrv  46601  sumnnodd  46750  liminfgval  46880  ioodvbdlimc2lem  47052  itgsin0pilem1  47068  stoweidlem55  47173  wallispilem1  47183  wallispilem2  47184  wallispilem4  47186  wallispi2lem1  47189  wallispi2lem2  47190  dirkerval  47209  fourierdlem2  47227  fourierdlem3  47228  fourierdlem29  47254  fourierdlem62  47286  fourierdlem80  47304  fourierdlem103  47327  fourierdlem104  47328  fourierswlem  47348  fouriersw  47349  iundjiunlem  47577  carageniuncllem2  47640  0ome  47647  hoidmv1le  47712  hoidmvlelem3  47715  smflimsuplem7  47944  sqrtnnaa  48021  sqrtnzqaa  48022  sqrtnpoly  48051  iccpval  48605  fppr  48932  bigoval  49769  ackval0  49900  ackval41a  49914  oppcinito  50465  oppctermo  50466  dfinito4  50744  prstcval  50797  mndtcval  50825  setc1onsubc  50848  parswapval  50884  lmdfval2  50946  cmdfval2  50947  vsetrec  50979  onsetreclem1  50981  elpglem3  50989  pgindnf  50992  sinhval-named  51012  coshval-named  51013  tanhval-named  51014  secval  51023  cscval  51024  cotval  51025  aacllem  51122