Theorem fvmpt 6993

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3457   ↦ cmpt 5194  ‘cfv 6540

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548

This theorem is used by:  fvmptex  7008  fvmptrabfv  7026  mptfvmpt  7233  fvmptopab  7474  ofval  7695  caofinvl  7716  fvresex  7963  1stval  7994  2ndval  7995  reldm  8047  curry1val  8106  curry2val  8110  fsplitfpar  8119  fnwelem  8133  brtpos2  8234  onovuni  8335  tz7.44-1  8399  oasuc  8515  oesuclem  8516  omsuc  8517  onasuc  8519  onmsuc  8520  fsetfocdm  8864  fvmptmap  8885  xpcomco  9062  unxpdomlem1  9223  unfilem2  9273  ordtypelem3  9489  ixpiunwdom  9559  inf3lema  9600  noinfep  9636  cantnfval  9644  cantnflem1d  9664  cantnflem1  9665  ssttrcl  9691  ttrcltr  9692  ttrclselem2  9702  r1sucg  9748  r0weon  10012  infxpenc2lem1  10019  fseqenlem1  10024  fseqenlem2  10025  dfac8alem  10029  ac5num  10036  acni2  10046  dfac4  10122  dfac2a  10129  dfacacn  10141  dfac12lem1  10143  ackbij1lem7  10224  ackbij2lem2  10238  ackbij2lem3  10239  cfsmolem  10269  fin23lem28  10339  fin23lem39  10349  isf32lem6  10357  isf32lem7  10358  isf32lem8  10359  fin1a2lem3  10401  itunifval  10415  itunisuc  10418  axdc2lem  10447  axdc3lem2  10450  axcclem  10456  zorn2lem1  10495  negiso  12210  infrenegsup  12213  uzval  12880  flval  13845  ceilval  13889  ceilval2  13891  monoord2  14087  seqf1olem2  14096  seqf1o  14097  seqdistr  14107  serle  14111  seqof  14113  swrdfv  14706  revval  14819  revfv  14822  wwlktovf1  15018  wwlktovfo  15019  sgnval  15149  cjval  15177  reval  15181  imval  15182  sqrtval  15312  absval  15313  limsupval  15549  limsupgval  15551  climmpt  15646  climle  15715  rlimdiv  15721  isercolllem1  15740  isercoll2  15744  caurcvg2  15753  fsumser  15804  isumadd  15841  fsumcnv  15847  fsumrev  15853  fsumshft  15854  iserabs  15890  cvgcmp  15891  cvgcmpce  15893  incexclem  15913  isumless  15922  divcnvshft  15932  supcvg  15933  harmonic  15936  trireciplem  15939  trirecip  15940  expcnv  15941  explecnv  15942  geolim  15947  geolim2  15948  geo2lim  15952  geomulcvg  15953  geoisum  15954  geoisumr  15955  geoisum1  15956  geoisum1c  15957  cvgrat  15960  mertenslem2  15962  mertens  15963  prodfdiv  15973  fprodser  16026  fprodshft  16053  fprodrev  16054  fprodcnv  16060  iprodmul  16080  bpolylem  16124  eftval  16152  efval  16155  efcvgfsum  16162  ege2le3  16166  eftlub  16187  eflegeo  16199  sinval  16200  cosval  16201  tanval  16206  eirrlem  16282  rpnnen2lem1  16292  rpnnen2lem2  16293  bitsfval  16503  bitsinv2  16523  bitsinv  16528  sadcf  16533  sadc0  16534  sadcp1  16535  smupf  16558  smup0  16559  smupp1  16560  qnumval  16818  qdenval  16819  phival  16848  crth  16859  phimullem  16860  eulerthlem2  16863  phisum  16872  odzval  16873  iserodd  16917  pcmpt  16974  prmreclem1  16998  prmreclem2  16999  prmreclem4  17001  prmreclem5  17002  prmreclem6  17003  1arithlem1  17005  1arithlem2  17006  vdwapfval  17053  vdwlem2  17064  vdwlem6  17068  vdwlem8  17070  vdwlem9  17071  ramub1lem2  17109  ramcl  17111  prmoval  17115  strfvnd  17267  topnval  17509  prdsplusgfval  17549  prdsmulrfval  17551  isacs  17729  acsfn  17737  homffval  17768  comfffval  17776  oppcval  17791  monfval  17811  oppcmon  17817  sectffval  17829  invffval  17837  isoval  17844  idfuval  17955  homafval  18108  arwval  18122  coafval  18143  yonedainv  18359  oduval  18366  pltfval  18407  lubfval  18426  lubval  18432  glbfval  18439  glbval  18445  p0val  18503  p1val  18504  ipoval  18608  plusffval  18726  grpidval  18744  issubmgm  18792  issubm  18898  prdspjmhm  18925  efmnd  18966  smndex1gbas  18998  smndex1gid  19000  smndex1igid  19002  smndex1igidOLD  19003  grpinvfval  19089  grpinvval  19091  grpsubfval  19094  grpsubfvalALT  19095  grplactval  19152  prdsinvlem  19159  mulgfval  19179  mulgfvalALT  19180  pwsmulg  19229  issubg  19236  isnsg  19265  cycsubmel  19315  cycsubgcl  19321  conjghm  19363  conjnmz  19366  cntrval  19433  cntzfval  19434  cntzval  19435  oppgval  19461  psgnfval  19614  psgnval  19621  odfval  19646  odval  19648  sylow1lem4  19715  pgpssslw  19728  sylow2blem3  19736  sylow3lem2  19742  lsmfval  19752  pj1fval  19808  efgval  19831  efgsval  19845  frgpval  19872  vrgpval  19881  mulgmhm  19941  mulgghm  19942  ablfaclem1  20201  mgpval  20263  srglmhm  20347  srgrmhm  20348  ringlghm  20441  ringrghm  20442  pwspjmhmmgpd  20455  pwsexpg  20456  opprval  20466  dvdsrval  20489  isunit  20501  invrfval  20517  dvrfval  20530  isirred  20547  issubrng  20696  issubrg  20720  rgspnval  20761  rrgval  20846  fidomndrnglem  20926  issdrg  20941  abvfval  20963  abvtrivd  20985  staffval  20994  stafval  20995  scaffval  21051  lmodvsghm  21094  lssset  21104  lspfval  21144  islbs  21247  sraval  21346  rlmval  21362  2idlval  21440  lpival  21542  expmhm  21636  expghm  21675  mulgghm2  21676  mulgrhm  21677  zrhval  21707  zrhmulg  21709  zlmval  21715  chrval  21723  znval  21735  znzrhval  21746  evpmss  21786  psgnevpmb  21787  ip0l  21836  ipffval  21848  ocvfval  21866  ocvval  21867  cssval  21882  thlval  21895  pjfval  21906  pjval  21910  isobs  21920  prdsinvgd2  21942  uvcresum  21993  frlmup1  21998  frlmup2  21999  islinds  22009  islindf5  22039  aspval  22072  asclval  22079  psrmulval  22144  psrlidm  22161  psrridm  22162  psrascl  22178  mvrval  22181  mvrval2  22182  mplmonmul  22237  evlslem3  22281  evlslem1  22283  evlsval  22287  evlssca  22295  evlsvar  22296  psdmul  22379  psdmvr  22382  psr1val  22396  vr1val  22402  ply1val  22404  coe1fval  22415  coe1fv  22416  coe1tmmul2  22487  coe1tmmul  22488  coe1tmmul2fv  22489  coe1pwmulfv  22491  evls1val  22530  evl1fval  22538  evl1val  22539  mamulid  22648  mamurid  22649  mdetleib  22794  mdetleib1  22798  mdetunilem9  22827  mdetuni0  22828  mdetmul  22830  cpmidpmatlem1  23077  ordtval  23396  cnpval  23443  ptpjpre1  23779  ptpjopn  23820  dfac14  23826  upxp  23831  uptx  23833  hauseqlcld  23854  txlm  23856  xkoptsub  23862  xkoinjcn  23895  kqval  23934  xpstopnlem1  24017  fmval  24151  flfval  24198  ptcmplem2  24261  ptcmplem3  24262  symgtgp  24314  qustgpopn  24328  ussval  24467  iscfilu  24495  ispsmet  24512  ismet  24531  isxmet  24532  mopnval  24646  prdsxmslem2  24737  nmfval  24796  nmval  24797  nmoval  24923  metdsval  25056  divcn  25078  mulc1cncf  25115  icopnfhmeo  25153  iccpnfhmeo  25155  xrhmeo  25156  cnheiborlem  25164  evth  25169  evth2  25170  lebnumlem3  25173  isphtpy  25191  isphtpc  25204  pcofval  25220  pcovalg  25222  pco1  25225  pcopt  25232  pcopt2  25233  pcoass  25234  pcorevcl  25235  pcorevlem  25236  pcorev2  25238  pi1xfrcnv  25267  cphnm  25403  tcphval  25428  tcphnmval  25439  cfilfval  25474  iscmet  25494  iscmet3lem3  25500  rrxval  25597  ehlval  25624  ivth2  25665  ovolval  25683  ovollb2lem  25698  ovolunlem1a  25706  ovolunlem1  25707  ovoliunlem1  25712  ovoliunlem2  25713  ovolicc1  25726  voliunlem1  25760  voliunlem2  25761  voliunlem3  25762  volsup  25766  ioorval  25784  uniioombllem3  25795  uniioombllem6  25798  volsup2  25815  volcn  25816  volivth  25817  vitalilem2  25819  vitalilem3  25820  vitalilem4  25821  vitali  25823  mbfmax  25859  mbfimaopnlem  25865  itg1val  25893  i1f1lem  25899  itg11  25901  itg1addlem4  25909  itg1mulc  25914  i1fres  25915  itg1climres  25924  mbfi1fseqlem2  25926  mbfi1fseqlem3  25927  mbfi1fseqlem6  25930  mbfi1flimlem  25932  mbfi1flim  25933  mbfmullem2  25934  itg2seq  25952  itg2uba  25953  itg2splitlem  25958  itg2monolem1  25960  itg2monolem2  25961  itg2monolem3  25962  itg2mono  25963  itg2i1fseqle  25964  itg2i1fseq  25965  itg2i1fseq2  25966  itg2addlem  25968  itg2cnlem1  25971  itg2cn  25973  limccnp2  26102  dvnff  26133  dvnp1  26135  cpnfval  26142  elcpn  26144  dvrec  26165  dvcnvlem  26186  dveflem  26189  dvef  26190  dvferm1  26195  dvferm2  26197  rolle  26200  dvlip  26203  dvlipcn  26204  dv11cn  26211  dvivthlem1  26218  dvivth  26220  lhop1lem  26223  ftc1lem1  26245  ftc1lem5  26250  ftc2  26254  itgsubstlem  26258  tdeglem3  26267  tdeglem4  26268  mdegval  26271  mdegmullem  26286  deg1fval  26288  deg1ldg  26300  deg1leb  26303  coe1mul3  26307  uc1pval  26348  mon1pval  26350  mon1pid  26362  q1pval  26363  r1pval  26366  ply1remlem  26373  ig1pval  26384  plyval  26401  elply2  26404  plyeq0lem  26418  coeval  26431  dgrval  26436  coeid2  26447  coemullem  26458  coemul  26460  plymulidp  26494  elqaalem1  26531  elqaalem2  26532  elqaalem3  26533  iaa  26539  aareccl  26540  aannenlem1  26542  geolim3  26553  aaliou3lem1  26556  aaliou3lem2  26557  aaliou3lem5  26561  aaliou3lem6  26562  aaliou3lem7  26563  aaliou3  26565  aaliou3r  26566  tayl0  26576  taylthlem1  26587  taylthlem2  26588  ulmshftlem  26603  ulmshft  26604  ulmuni  26606  ulmcau  26609  ulmdvlem1  26614  ulmdvlem3  26616  mtest  26618  mtestbdd  26619  mbfulm  26620  iblulm  26621  itgulm  26622  pserval  26624  pserval2  26625  radcnvlem1  26627  radcnvlem2  26628  dvradcnv  26635  pserulm  26636  pserdvlem2  26642  pserdv  26643  abelthlem1  26645  abelthlem3  26647  abelthlem4  26648  abelthlem5  26649  abelthlem6  26650  abelthlem7  26652  abelthlem8  26653  abelthlem9  26654  resinf1o  26752  efif1olem4  26761  eff1olem  26764  logcnlem5  26862  logtayllem  26875  logtayl  26876  logtaylsum  26877  logtayl2  26878  logccv  26879  asinval  27098  acosval  27099  atanval  27100  atantayl  27153  leibpilem2  27157  leibpi  27158  leibpisum  27159  log2cnv  27160  log2tlbnd  27161  areaval  27180  efrlim  27185  dfef2  27186  amgmlem  27205  emcllem2  27212  emcllem3  27213  emcllem4  27214  emcllem5  27215  emcllem6  27216  emcllem7  27217  zetacvg  27230  lgamgulmlem4  27247  lgamgulmlem5  27248  lgamgulm2  27251  lgamcvglem  27255  igamval  27262  lgamcvg2  27270  gamcvg2lem  27274  ftalem7  27294  basellem2  27297  basellem3  27298  basellem4  27299  basellem5  27300  basellem6  27301  basellem8  27303  basellem9  27304  chtval  27325  vmaval  27328  chpval  27337  ppival  27342  muval  27347  prmorcht  27393  sqff1o  27397  dvdsflsumcom  27403  musum  27406  muinv  27408  sgmppw  27412  fsumvma  27428  pclogsum  27430  dchrfi  27470  bposlem5  27503  bposlem7  27505  bposlem8  27506  bposlem9  27507  lgsfval  27517  lgsdir  27547  lgsdilem2  27548  lgsdi  27549  lgsne0  27550  lgsqrlem2  27562  lgsqrlem4  27564  lgseisenlem2  27591  dchrmusum2  27709  dchrvmasumlem1  27710  dchrvmasumiflem1  27716  dchrvmaeq0  27719  dchrisum0fval  27720  dchrisum0re  27728  mulog2sumlem1  27749  pntrval  27777  pntsval  27787  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntlem3  27824  abvcxp  27830  padicfval  27831  padicval  27832  padicabv  27845  ostth1  27848  ostth2  27852  ostth3  27853  nosupfv  27921  noinffv  27936  newval  28079  leftval  28093  rightval  28094  iscgrg  28832  legval  28904  ishpg  29092  iscgra  29171  isinag  29210  isleag  29219  iseqlg  29239  ttgval  29279  elee  29298  axsegconlem1  29322  axsegconlem9  29330  axsegconlem10  29331  axpasch  29346  axlowdimlem15  29361  axlowdim  29366  axeuclidlem  29367  axcontlem2  29370  eengv  29384  vtxval  29405  iedgval  29406  edgval  29454  vtxdgval  29876  wwlksnextinj  30315  wwlksnextsurj  30316  clwwlkfv  30466  clwwlknonmpo  30507  fusgreg2wsplem  30755  fusgreghash2wsp  30760  numclwwlk1lem2fv  30778  gidval  30935  grpoinvval  30946  bafval  31027  imsval  31108  dipfval  31125  sspval  31146  nmooval  31186  hmoval  31233  ipasslem8  31260  ipasslem9  31261  ipblnfi  31278  ubthlem2  31294  htthlem  31340  normval  31547  ocval  31703  occllem  31726  hsupval  31757  pjhfval  31819  pjhval  31820  chscllem2  32061  chscllem3  32062  hosval  32163  homval  32164  hodval  32165  hfsval  32166  hfmval  32167  brafval  32366  braval  32367  kbval  32377  eigvalval  32383  cnlnadjlem1  32490  nmopadjlei  32511  hmopidmchi  32574  strlem2  32674  hstrlem2  32682  cdj3lem2  32858  ofpreima  33081  psgnfzto1stlem  33484  evpmval  33529  altgnsg  33533  inftmrel  33564  isinftm  33565  qusker  33733  qusvscpbl  33735  qusvsval  33736  mxidlval  33808  idlsrgval  33857  psrmonmul  34004  dimval  34055  dimvalfi  34056  smatfval  34249  lmatval  34267  locfinreflem  34294  rspecval  34318  rmulccn  34382  xrmulc1cn  34384  xrge0iifcv  34388  xrge0iifiso  34389  xrge0iifhom  34391  xrge0iif1  34392  qqhval  34426  rrhval  34450  xrhval  34472  ddeval1  34689  ddeval0  34690  sxbrsigalem0  34726  sxbrsigalem3  34727  eulerpartlemgv  34828  rrvmbfm  34897  dstrvval  34926  coinflippv  34939  ballotlem2  34944  ballotlemfval  34945  ballotlemi  34956  ballotlemsval  34964  ballotlemrval  34973  ballotth  34993  signstfv  35015  signsvvfval  35030  kardval  35622  kard0  35624  onvf1odlem3  35646  derangval  35696  subfacval  35702  erdszelem3  35722  erdszelem9  35728  erdszelem10  35729  txpconn  35761  indispconn  35763  cvxpconn  35771  cvmlift2lem2  35833  cvmlift2lem3  35834  cvmlift2lem7  35838  cvmliftphtlem  35846  cvmlift3lem4  35851  snmlfval  35859  snmlval  35860  gonafv  35879  mvtval  36029  mrsubffval  36036  mrsubcv  36039  mrsubrn  36042  elmrsubrn  36049  msubffval  36052  mvhval  36063  mpstval  36064  mstaval  36073  mclsval  36092  mppsval  36101  sinccvglem  36201  circum  36203  divcnvlin  36262  iprodefisum  36270  iprodgam  36271  faclimlem1  36272  faclimlem2  36273  faclim  36275  iprodfac  36276  faclim2  36277  dfrdg2  36322  findabrcl  37022  dnival  37117  bj-evalval  37774  bj-inftyexpitaudisj  37906  bj-inftyexpiinv  37909  bj-inftyexpidisj  37911  curfv  38308  finixpnum  38313  poimirlem16  38344  poimir  38361  broucube  38362  mblfinlem2  38366  voliunnfl  38372  volsupnfl  38373  itg2addnclem  38379  itg2addnclem3  38381  ftc1cnnc  38400  ftc1anclem5  38405  ftc1anclem6  38406  ftc1anclem7  38407  ftc1anc  38409  ftc2nc  38410  fvopabf4g  38431  sdclem2  38451  fdc  38454  lmclim2  38467  geomcau  38468  istotbnd  38478  isbnd  38489  prdsbnd2  38504  heiborlem6  38525  heiborlem7  38526  heiborlem8  38527  rrnval  38536  rrncmslem  38541  idlval  38722  pridlval  38742  maxidlval  38748  lshpset  39810  lsatset  39822  lcvfbr  39852  lflset  39891  lflnegcl  39907  lshpkrlem1  39942  lshpkrlem2  39943  lshpkrlem3  39944  ldualset  39957  cmtfvalN  40042  cvrfval  40100  pats  40117  llnset  40337  lplnset  40361  lvolset  40404  lineset  40570  pointsetN  40573  psubspset  40576  pmapval  40589  paddfval  40629  pclfvalN  40721  polfvalN  40736  polvalN  40737  psubclsetN  40768  watvalN  40825  lhpset  40827  lautset  40914  pautsetN  40930  ldilset  40941  ltrnset  40950  dilsetN  40985  trnsetN  40988  trlset  40993  trlval  40994  tgrpset  41577  tendoset  41591  tendo02  41619  erngset  41632  erngset-rN  41640  cdlemksv  41676  dvaset  41837  dvaplusgv  41842  diafval  41863  diaval  41864  dvhset  41913  cdlemm10N  41950  docafvalN  41954  djafvalN  41966  dibfval  41973  dibval  41974  dicfval  42007  dicval  42008  dihval  42064  dochfval  42182  djhfval  42229  dochfl1  42308  lpolsetN  42314  lcdval  42421  mapdhval  42556  hvmapfval  42591  hdmap1fval  42628  fimgmcyc  43360  prjspval  43393  isnacs  43493  mzpclval  43514  mzpsubst  43537  mzprename  43538  mzpcompact2lem  43540  eldiophb  43546  diophrw  43548  eldioph2  43551  diophin  43561  diophun  43562  diophren  43598  pell1qrval  43631  pell14qrval  43633  pell1234qrval  43635  pellfundval  43665  rmxypairf1o  43696  rmxyval  43700  mzpcong  43757  pw2f1ocnv  43822  dnnumch1  43829  dfac11  43847  hbtlem1  43908  hbtlem7  43910  elmnc  43921  dgraaval  43929  mpaaval  43936  itgoval  43946  flcidc  43955  mendval  43964  cytpval  43987  cantnfub  44106  cantnfresb  44109  tfsconcatrev  44133  elcnvlem  44385  comptiunov2i  44490  dftrcl3  44504  trclfvcom  44507  cnvtrclfv  44508  cotrcltrcl  44509  trclimalb2  44510  trclfvdecomr  44512  dfrtrcl3  44517  dfrtrcl4  44522  clsk1indlem0  44825  clsk1indlem2  44826  clsk1indlem3  44827  clsk1indlem4  44828  clsk1indlem1  44829  k0004val  44934  lhe4.4ex1a  45097  addrfv  45235  subrfv  45236  mulvfv  45237  monoord2xrv  46255  sumnnodd  46404  liminfgval  46534  ioodvbdlimc2lem  46706  itgsin0pilem1  46722  stoweidlem55  46827  wallispilem1  46837  wallispilem2  46838  wallispilem4  46840  wallispi2lem1  46843  wallispi2lem2  46844  dirkerval  46863  fourierdlem2  46881  fourierdlem3  46882  fourierdlem29  46908  fourierdlem62  46940  fourierdlem80  46958  fourierdlem103  46981  fourierdlem104  46982  fourierswlem  47002  fouriersw  47003  iundjiunlem  47231  carageniuncllem2  47294  0ome  47301  hoidmv1le  47366  hoidmvlelem3  47369  smflimsuplem7  47598  sqrtnnaa  47662  sqrtnzqaa  47663  iccpval  48222  fppr  48549  bigoval  49386  ackval0  49517  ackval41a  49531  eenglngeehlnm  49576  oppcinito  50070  oppctermo  50071  dfinito4  50336  prstcval  50386  mndtcval  50414  setc1onsubc  50437  lmdfval2  50490  cmdfval2  50491  vsetrec  50538  onsetreclem1  50540  elpglem3  50548  pgindnf  50551  sinhval-named  50571  coshval-named  50572  tanhval-named  50573  secval  50582  cscval  50583  cotval  50584  aacllem  50678