Theorem fvmpt 6941

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ↦ cmpt 5167  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptex  6956  fvmptrabfv  6974  mptfvmpt  7176  fvmptopab  7415  ofval  7635  caofinvl  7656  fvresex  7906  1stval  7937  2ndval  7938  reldm  7990  curry1val  8048  curry2val  8052  fsplitfpar  8061  fnwelem  8074  brtpos2  8175  onovuni  8275  tz7.44-1  8338  oasuc  8452  oesuclem  8453  omsuc  8454  onasuc  8456  onmsuc  8457  fsetfocdm  8801  fvmptmap  8822  xpcomco  8998  unxpdomlem1  9159  unfilem2  9209  ordtypelem3  9428  ixpiunwdom  9498  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  20515  issubrg  20539  rgspnval  20580  rrgval  20665  fidomndrnglem  20740  issdrg  20756  abvfval  20778  abvtrivd  20800  staffval  20809  stafval  20810  scaffval  20866  lmodvsghm  20909  lssset  20919  lspfval  20959  islbs  21063  sraval  21162  rlmval  21178  2idlval  21241  lpival  21314  expmhm  21426  expghm  21465  mulgghm2  21466  mulgrhm  21467  zrhval  21497  zrhmulg  21499  zlmval  21505  chrval  21513  znval  21525  znzrhval  21536  evpmss  21576  psgnevpmb  21577  ip0l  21626  ipffval  21638  ocvfval  21656  ocvval  21657  cssval  21672  thlval  21685  pjfval  21696  pjval  21700  isobs  21710  prdsinvgd2  21732  uvcresum  21783  frlmup1  21788  frlmup2  21789  islinds  21799  islindf5  21829  aspval  21862  asclval  21869  psrmulval  21933  psrlidm  21950  psrridm  21951  psrascl  21967  mvrval  21970  mvrval2  21971  mplmonmul  22024  evlslem3  22068  evlslem1  22070  evlsval  22074  evlssca  22082  evlsvar  22083  psdmul  22142  psdmvr  22145  psr1val  22159  vr1val  22165  ply1val  22167  coe1fval  22179  coe1fv  22180  coe1tmmul2  22251  coe1tmmul  22252  coe1tmmul2fv  22253  coe1pwmulfv  22255  evls1val  22295  evl1fval  22303  evl1val  22304  mamulid  22416  mamurid  22417  mdetleib  22562  mdetleib1  22566  mdetunilem9  22595  mdetuni0  22596  mdetmul  22598  cpmidpmatlem1  22845  ordtval  23164  cnpval  23211  ptpjpre1  23546  ptpjopn  23587  dfac14  23593  upxp  23598  uptx  23600  hauseqlcld  23621  txlm  23623  xkoptsub  23629  xkoinjcn  23662  kqval  23701  xpstopnlem1  23784  fmval  23918  flfval  23965  ptcmplem2  24028  ptcmplem3  24029  symgtgp  24081  qustgpopn  24095  ussval  24234  iscfilu  24262  ispsmet  24279  ismet  24298  isxmet  24299  mopnval  24413  prdsxmslem2  24504  nmfval  24563  nmval  24564  nmoval  24690  metdsval  24823  divcn  24845  mulc1cncf  24882  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  cnheiborlem  24931  evth  24936  evth2  24937  lebnumlem3  24940  isphtpy  24958  isphtpc  24971  pcofval  24987  pcovalg  24989  pco1  24992  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevcl  25002  pcorevlem  25003  pcorev2  25005  pi1xfrcnv  25034  cphnm  25170  tcphval  25195  tcphnmval  25206  cfilfval  25241  iscmet  25261  iscmet3lem3  25267  rrxval  25364  ehlval  25391  ivth2  25432  ovolval  25450  ovollb2lem  25465  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliunlem2  25480  ovolicc1  25493  voliunlem1  25527  voliunlem2  25528  voliunlem3  25529  volsup  25533  ioorval  25551  uniioombllem3  25562  uniioombllem6  25565  volsup2  25582  volcn  25583  volivth  25584  vitalilem2  25586  vitalilem3  25587  vitalilem4  25588  vitali  25590  mbfmax  25626  mbfimaopnlem  25632  itg1val  25660  i1f1lem  25666  itg11  25668  itg1addlem4  25676  itg1mulc  25681  i1fres  25682  itg1climres  25691  mbfi1fseqlem2  25693  mbfi1fseqlem3  25694  mbfi1fseqlem6  25697  mbfi1flimlem  25699  mbfi1flim  25700  mbfmullem2  25701  itg2seq  25719  itg2uba  25720  itg2splitlem  25725  itg2monolem1  25727  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2i1fseqle  25731  itg2i1fseq  25732  itg2i1fseq2  25733  itg2addlem  25735  itg2cnlem1  25738  itg2cn  25740  limccnp2  25869  dvnff  25900  dvnp1  25902  cpnfval  25909  elcpn  25911  dvrec  25932  dvcnvlem  25953  dveflem  25956  dvef  25957  dvferm1  25962  dvferm2  25964  rolle  25967  dvlip  25970  dvlipcn  25971  dv11cn  25978  dvivthlem1  25985  dvivth  25987  lhop1lem  25990  ftc1lem1  26012  ftc1lem5  26017  ftc2  26021  itgsubstlem  26025  tdeglem3  26034  tdeglem4  26035  mdegval  26038  mdegmullem  26053  deg1fval  26055  deg1ldg  26067  deg1leb  26070  coe1mul3  26074  uc1pval  26115  mon1pval  26117  mon1pid  26129  q1pval  26130  r1pval  26133  ply1remlem  26140  ig1pval  26151  plyval  26168  elply2  26171  plyeq0lem  26185  coeval  26198  dgrval  26203  coeid2  26214  coemullem  26225  coemul  26227  elqaalem1  26296  elqaalem2  26297  elqaalem3  26298  iaa  26302  aareccl  26303  aannenlem1  26305  geolim3  26316  aaliou3lem1  26319  aaliou3lem2  26320  aaliou3lem5  26324  aaliou3lem6  26325  aaliou3lem7  26326  aaliou3  26328  tayl0  26338  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmshftlem  26367  ulmshft  26368  ulmuni  26370  ulmcau  26373  ulmdvlem1  26378  ulmdvlem3  26380  mtest  26382  mtestbdd  26383  mbfulm  26384  iblulm  26385  itgulm  26386  pserval  26388  pserval2  26389  radcnvlem1  26391  radcnvlem2  26392  dvradcnv  26399  pserulm  26400  pserdvlem2  26406  pserdv  26407  abelthlem1  26409  abelthlem3  26411  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  resinf1o  26513  efif1olem4  26522  eff1olem  26525  logcnlem5  26623  logtayllem  26636  logtayl  26637  logtaylsum  26638  logtayl2  26639  logccv  26640  asinval  26859  acosval  26860  atanval  26861  atantayl  26914  leibpilem2  26918  leibpi  26919  leibpisum  26920  log2cnv  26921  log2tlbnd  26922  areaval  26941  efrlim  26946  efrlimOLD  26947  dfef2  26948  amgmlem  26967  emcllem2  26974  emcllem3  26975  emcllem4  26976  emcllem5  26977  emcllem6  26978  emcllem7  26979  zetacvg  26992  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulm2  27013  lgamcvglem  27017  igamval  27024  lgamcvg2  27032  gamcvg2lem  27036  ftalem7  27056  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  basellem6  27063  basellem8  27065  basellem9  27066  chtval  27087  vmaval  27090  chpval  27099  ppival  27104  muval  27109  prmorcht  27155  sqff1o  27159  dvdsflsumcom  27165  musum  27168  muinv  27170  sgmppw  27174  fsumvma  27190  pclogsum  27192  dchrfi  27232  bposlem5  27265  bposlem7  27267  bposlem8  27268  bposlem9  27269  lgsfval  27279  lgsdir  27309  lgsdilem2  27310  lgsdi  27311  lgsne0  27312  lgsqrlem2  27324  lgsqrlem4  27326  lgseisenlem2  27353  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasumiflem1  27478  dchrvmaeq0  27481  dchrisum0fval  27482  dchrisum0re  27490  mulog2sumlem1  27511  pntrval  27539  pntsval  27549  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntlem3  27586  abvcxp  27592  padicfval  27593  padicval  27594  padicabv  27607  ostth1  27610  ostth2  27614  ostth3  27615  nosupfv  27684  noinffv  27699  newval  27841  leftval  27855  rightval  27856  iscgrg  28594  legval  28666  ishpg  28841  iscgra  28891  isinag  28920  isleag  28929  iseqlg  28949  ttgval  28957  elee  28976  axsegconlem1  29000  axsegconlem9  29008  axsegconlem10  29009  axpasch  29024  axlowdimlem15  29039  axlowdim  29044  axeuclidlem  29045  axcontlem2  29048  eengv  29062  vtxval  29083  iedgval  29084  edgval  29132  vtxdgval  29552  wwlksnextinj  29982  wwlksnextsurj  29983  clwwlkfv  30133  clwwlknonmpo  30174  fusgreg2wsplem  30418  fusgreghash2wsp  30423  numclwwlk1lem2fv  30441  gidval  30598  grpoinvval  30609  bafval  30690  imsval  30771  dipfval  30788  sspval  30809  nmooval  30849  hmoval  30896  ipasslem8  30923  ipasslem9  30924  ipblnfi  30941  ubthlem2  30957  htthlem  31003  normval  31210  ocval  31366  occllem  31389  hsupval  31420  pjhfval  31482  pjhval  31483  chscllem2  31724  chscllem3  31725  hosval  31826  homval  31827  hodval  31828  hfsval  31829  hfmval  31830  brafval  32029  braval  32030  kbval  32040  eigvalval  32046  cnlnadjlem1  32153  nmopadjlei  32174  hmopidmchi  32237  strlem2  32337  hstrlem2  32345  cdj3lem2  32521  ofpreima  32753  psgnfzto1stlem  33176  evpmval  33221  altgnsg  33225  inftmrel  33256  isinftm  33257  qusker  33424  qusvscpbl  33426  qusvsval  33427  mxidlval  33536  idlsrgval  33578  psrmonmul  33709  dimval  33760  dimvalfi  33761  smatfval  33955  lmatval  33973  locfinreflem  34000  rspecval  34024  rmulccn  34088  xrmulc1cn  34090  xrge0iifcv  34094  xrge0iifiso  34095  xrge0iifhom  34097  xrge0iif1  34098  qqhval  34132  rrhval  34156  xrhval  34178  ddeval1  34394  ddeval0  34395  sxbrsigalem0  34431  sxbrsigalem3  34432  eulerpartlemgv  34533  rrvmbfm  34602  dstrvval  34631  coinflippv  34644  ballotlem2  34649  ballotlemfval  34650  ballotlemi  34661  ballotlemsval  34669  ballotlemrval  34678  ballotth  34698  plymulx  34708  signstfv  34723  signsvvfval  34738  onvf1odlem3  35303  derangval  35365  subfacval  35371  erdszelem3  35391  erdszelem9  35397  erdszelem10  35398  txpconn  35430  indispconn  35432  cvxpconn  35440  cvmlift2lem2  35502  cvmlift2lem3  35503  cvmlift2lem7  35507  cvmliftphtlem  35515  cvmlift3lem4  35520  snmlfval  35528  snmlval  35529  gonafv  35548  mvtval  35698  mrsubffval  35705  mrsubcv  35708  mrsubrn  35711  elmrsubrn  35718  msubffval  35721  mvhval  35732  mpstval  35733  mstaval  35742  mclsval  35761  mppsval  35770  sinccvglem  35870  circum  35872  divcnvlin  35931  iprodefisum  35939  iprodgam  35940  faclimlem1  35941  faclimlem2  35942  faclim  35944  iprodfac  35945  faclim2  35946  dfrdg2  35991  findabrcl  36652  dnival  36747  bj-evalval  37403  bj-inftyexpitaudisj  37535  bj-inftyexpiinv  37538  bj-inftyexpidisj  37540  curfv  37935  finixpnum  37940  poimirlem16  37971  poimir  37988  broucube  37989  mblfinlem2  37993  voliunnfl  37999  volsupnfl  38000  itg2addnclem  38006  itg2addnclem3  38008  ftc1cnnc  38027  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anc  38036  ftc2nc  38037  fvopabf4g  38057  sdclem2  38077  fdc  38080  lmclim2  38093  geomcau  38094  istotbnd  38104  isbnd  38115  prdsbnd2  38130  heiborlem6  38151  heiborlem7  38152  heiborlem8  38153  rrnval  38162  rrncmslem  38167  idlval  38348  pridlval  38368  maxidlval  38374  lshpset  39438  lsatset  39450  lcvfbr  39480  lflset  39519  lflnegcl  39535  lshpkrlem1  39570  lshpkrlem2  39571  lshpkrlem3  39572  ldualset  39585  cmtfvalN  39670  cvrfval  39728  pats  39745  llnset  39965  lplnset  39989  lvolset  40032  lineset  40198  pointsetN  40201  psubspset  40204  pmapval  40217  paddfval  40257  pclfvalN  40349  polfvalN  40364  polvalN  40365  psubclsetN  40396  watvalN  40453  lhpset  40455  lautset  40542  pautsetN  40558  ldilset  40569  ltrnset  40578  dilsetN  40613  trnsetN  40616  trlset  40621  trlval  40622  tgrpset  41205  tendoset  41219  tendo02  41247  erngset  41260  erngset-rN  41268  cdlemksv  41304  dvaset  41465  dvaplusgv  41470  diafval  41491  diaval  41492  dvhset  41541  cdlemm10N  41578  docafvalN  41582  djafvalN  41594  dibfval  41601  dibval  41602  dicfval  41635  dicval  41636  dihval  41692  dochfval  41810  djhfval  41857  dochfl1  41936  lpolsetN  41942  lcdval  42049  mapdhval  42184  hvmapfval  42219  hdmap1fval  42256  fimgmcyc  42993  prjspval  43050  isnacs  43150  mzpclval  43171  mzpsubst  43194  mzprename  43195  mzpcompact2lem  43197  eldiophb  43203  diophrw  43205  eldioph2  43208  diophin  43218  diophun  43219  diophren  43259  pell1qrval  43292  pell14qrval  43294  pell1234qrval  43296  pellfundval  43326  rmxypairf1o  43357  rmxyval  43361  mzpcong  43418  pw2f1ocnv  43483  dnnumch1  43490  dfac11  43508  hbtlem1  43569  hbtlem7  43571  elmnc  43582  dgraaval  43590  mpaaval  43597  itgoval  43607  flcidc  43616  mendval  43625  cytpval  43648  cantnfub  43767  cantnfresb  43770  tfsconcatrev  43794  elcnvlem  44046  comptiunov2i  44151  dftrcl3  44165  trclfvcom  44168  cnvtrclfv  44169  cotrcltrcl  44170  trclimalb2  44171  trclfvdecomr  44173  dfrtrcl3  44178  dfrtrcl4  44183  clsk1indlem0  44486  clsk1indlem2  44487  clsk1indlem3  44488  clsk1indlem4  44489  clsk1indlem1  44490  k0004val  44595  lhe4.4ex1a  44774  addrfv  44913  subrfv  44914  mulvfv  44915  monoord2xrv  45929  sumnnodd  46078  liminfgval  46208  ioodvbdlimc2lem  46380  itgsin0pilem1  46396  stoweidlem55  46501  wallispilem1  46511  wallispilem2  46512  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  dirkerval  46537  fourierdlem2  46555  fourierdlem3  46556  fourierdlem29  46582  fourierdlem62  46614  fourierdlem80  46632  fourierdlem103  46655  fourierdlem104  46656  fourierswlem  46676  fouriersw  46677  iundjiunlem  46905  carageniuncllem2  46968  0ome  46975  hoidmv1le  47040  hoidmvlelem3  47043  smflimsuplem7  47272  nthrucw  47332  iccpval  47887  fppr  48214  bigoval  49037  ackval0  49168  ackval41a  49182  eenglngeehlnm  49227  oppcinito  49722  oppctermo  49723  dfinito4  49988  prstcval  50038  mndtcval  50066  setc1onsubc  50089  lmdfval2  50142  cmdfval2  50143  vsetrec  50190  onsetreclem1  50192  elpglem3  50200  pgindnf  50203  sinhval-named  50223  coshval-named  50224  tanhval-named  50225  secval  50234  cscval  50235  cotval  50236  aacllem  50288