Theorem fvmpt 6989

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ↦ cmpt 5192  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544

This theorem is referenced by:  fvmptex  7004  fvmptrabfv  7022  mptfvmpt  7226  fvmptopab  7465  ofval  7685  caofinvl  7706  fvresex  7953  1stval  7984  2ndval  7985  reldm  8037  curry1val  8096  curry2val  8100  fsplitfpar  8109  fnwelem  8123  brtpos2  8224  onovuni  8325  tz7.44-1  8389  oasuc  8505  oesuclem  8506  omsuc  8507  onasuc  8509  onmsuc  8510  fsetfocdm  8854  fvmptmap  8875  xpcomco  9051  unxpdomlem1  9212  unfilem2  9262  ordtypelem3  9478  ixpiunwdom  9548  inf3lema  9589  noinfep  9625  cantnfval  9633  cantnflem1d  9653  cantnflem1  9654  ssttrcl  9680  ttrcltr  9681  ttrclselem2  9691  r1sucg  9737  r0weon  9992  infxpenc2lem1  9999  fseqenlem1  10004  fseqenlem2  10005  dfac8alem  10009  ac5num  10016  acni2  10026  dfac4  10102  dfac2a  10109  dfacacn  10121  dfac12lem1  10123  ackbij1lem7  10204  ackbij2lem2  10218  ackbij2lem3  10219  cfsmolem  10249  fin23lem28  10319  fin23lem39  10329  isf32lem6  10337  isf32lem7  10338  isf32lem8  10339  fin1a2lem3  10381  itunifval  10395  itunisuc  10398  axdc2lem  10427  axdc3lem2  10430  axcclem  10436  zorn2lem1  10475  negiso  12190  infrenegsup  12193  uzval  12859  flval  13823  ceilval  13867  ceilval2  13869  monoord2  14065  seqf1olem2  14074  seqf1o  14075  seqdistr  14085  serle  14089  seqof  14091  swrdfv  14682  revval  14793  revfv  14796  wwlktovf1  14990  wwlktovfo  14991  sgnval  15121  cjval  15149  reval  15153  imval  15154  sqrtval  15284  absval  15285  limsupval  15521  limsupgval  15523  climmpt  15618  climle  15687  rlimdiv  15693  isercolllem1  15712  isercoll2  15716  caurcvg2  15725  fsumser  15777  isumadd  15814  fsumcnv  15820  fsumrev  15826  fsumshft  15827  iserabs  15863  cvgcmp  15864  cvgcmpce  15866  incexclem  15886  isumless  15895  divcnvshft  15905  supcvg  15906  harmonic  15909  trireciplem  15912  trirecip  15913  expcnv  15914  explecnv  15915  geolim  15920  geolim2  15921  geo2lim  15925  geomulcvg  15926  geoisum  15927  geoisumr  15928  geoisum1  15929  geoisum1c  15930  cvgrat  15933  mertenslem2  15935  mertens  15936  prodfdiv  15946  fprodser  15999  fprodshft  16026  fprodrev  16027  fprodcnv  16033  iprodmul  16053  bpolylem  16097  eftval  16125  efval  16128  efcvgfsum  16135  ege2le3  16139  eftlub  16160  eflegeo  16172  sinval  16173  cosval  16174  tanval  16179  eirrlem  16255  rpnnen2lem1  16265  rpnnen2lem2  16266  bitsfval  16476  bitsinv2  16496  bitsinv  16501  sadcf  16506  sadc0  16507  sadcp1  16508  smupf  16531  smup0  16532  smupp1  16533  qnumval  16791  qdenval  16792  phival  16821  crth  16832  phimullem  16833  eulerthlem2  16836  phisum  16845  odzval  16846  iserodd  16890  pcmpt  16947  prmreclem1  16971  prmreclem2  16972  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  1arithlem1  16978  1arithlem2  16979  vdwapfval  17026  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  vdwlem9  17044  ramub1lem2  17082  ramcl  17084  prmoval  17088  strfvnd  17240  topnval  17482  prdsplusgfval  17522  prdsmulrfval  17524  isacs  17702  acsfn  17710  homffval  17741  comfffval  17749  oppcval  17764  monfval  17784  oppcmon  17790  sectffval  17802  invffval  17810  isoval  17817  idfuval  17928  homafval  18081  arwval  18095  coafval  18116  yonedainv  18332  oduval  18339  pltfval  18380  lubfval  18399  lubval  18405  glbfval  18412  glbval  18418  p0val  18476  p1val  18477  ipoval  18581  plusffval  18699  grpidval  18714  issubmgm  18755  issubm  18856  prdspjmhm  18883  efmnd  18924  smndex1gbas  18956  smndex1gid  18958  smndex1igid  18960  smndex1igidOLD  18961  grpinvfval  19040  grpinvval  19042  grpsubfval  19045  grpsubfvalALT  19046  grplactval  19103  prdsinvlem  19110  mulgfval  19130  mulgfvalALT  19131  pwsmulg  19180  issubg  19187  isnsg  19216  cycsubmel  19266  cycsubgcl  19272  conjghm  19314  conjnmz  19317  cntrval  19384  cntzfval  19385  cntzval  19386  oppgval  19412  psgnfval  19565  psgnval  19572  odfval  19597  odval  19599  sylow1lem4  19666  pgpssslw  19679  sylow2blem3  19687  sylow3lem2  19693  lsmfval  19703  pj1fval  19759  efgval  19782  efgsval  19796  frgpval  19823  vrgpval  19832  mulgmhm  19892  mulgghm  19893  ablfaclem1  20152  mgpval  20214  srglmhm  20298  srgrmhm  20299  ringlghm  20391  ringrghm  20392  pwspjmhmmgpd  20405  pwsexpg  20406  opprval  20416  dvdsrval  20439  isunit  20451  invrfval  20467  dvrfval  20480  isirred  20497  issubrng  20646  issubrg  20670  rgspnval  20711  rrgval  20796  fidomndrnglem  20876  issdrg  20891  abvfval  20913  abvtrivd  20935  staffval  20944  stafval  20945  scaffval  21001  lmodvsghm  21044  lssset  21054  lspfval  21094  islbs  21197  sraval  21296  rlmval  21312  2idlval  21390  lpival  21492  expmhm  21586  expghm  21625  mulgghm2  21626  mulgrhm  21627  zrhval  21657  zrhmulg  21659  zlmval  21665  chrval  21673  znval  21685  znzrhval  21696  evpmss  21736  psgnevpmb  21737  ip0l  21786  ipffval  21798  ocvfval  21816  ocvval  21817  cssval  21832  thlval  21845  pjfval  21856  pjval  21860  isobs  21870  prdsinvgd2  21892  uvcresum  21943  frlmup1  21948  frlmup2  21949  islinds  21959  islindf5  21989  aspval  22022  asclval  22029  psrmulval  22094  psrlidm  22111  psrridm  22112  psrascl  22128  mvrval  22131  mvrval2  22132  mplmonmul  22187  evlslem3  22231  evlslem1  22233  evlsval  22237  evlssca  22245  evlsvar  22246  psdmul  22329  psdmvr  22332  psr1val  22346  vr1val  22352  ply1val  22354  coe1fval  22365  coe1fv  22366  coe1tmmul2  22437  coe1tmmul  22438  coe1tmmul2fv  22439  coe1pwmulfv  22441  evls1val  22480  evl1fval  22488  evl1val  22489  mamulid  22598  mamurid  22599  mdetleib  22744  mdetleib1  22748  mdetunilem9  22777  mdetuni0  22778  mdetmul  22780  cpmidpmatlem1  23027  ordtval  23346  cnpval  23393  ptpjpre1  23728  ptpjopn  23769  dfac14  23775  upxp  23780  uptx  23782  hauseqlcld  23803  txlm  23805  xkoptsub  23811  xkoinjcn  23844  kqval  23883  xpstopnlem1  23966  fmval  24100  flfval  24147  ptcmplem2  24210  ptcmplem3  24211  symgtgp  24263  qustgpopn  24277  ussval  24416  iscfilu  24444  ispsmet  24461  ismet  24480  isxmet  24481  mopnval  24595  prdsxmslem2  24686  nmfval  24745  nmval  24746  nmoval  24872  metdsval  25005  divcn  25027  mulc1cncf  25064  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  cnheiborlem  25113  evth  25118  evth2  25119  lebnumlem3  25122  isphtpy  25140  isphtpc  25153  pcofval  25169  pcovalg  25171  pco1  25174  pcopt  25181  pcopt2  25182  pcoass  25183  pcorevcl  25184  pcorevlem  25185  pcorev2  25187  pi1xfrcnv  25216  cphnm  25352  tcphval  25377  tcphnmval  25388  cfilfval  25423  iscmet  25443  iscmet3lem3  25449  rrxval  25546  ehlval  25573  ivth2  25614  ovolval  25632  ovollb2lem  25647  ovolunlem1a  25655  ovolunlem1  25656  ovoliunlem1  25661  ovoliunlem2  25662  ovolicc1  25675  voliunlem1  25709  voliunlem2  25710  voliunlem3  25711  volsup  25715  ioorval  25733  uniioombllem3  25744  uniioombllem6  25747  volsup2  25764  volcn  25765  volivth  25766  vitalilem2  25768  vitalilem3  25769  vitalilem4  25770  vitali  25772  mbfmax  25808  mbfimaopnlem  25814  itg1val  25842  i1f1lem  25848  itg11  25850  itg1addlem4  25858  itg1mulc  25863  i1fres  25864  itg1climres  25873  mbfi1fseqlem2  25875  mbfi1fseqlem3  25876  mbfi1fseqlem6  25879  mbfi1flimlem  25881  mbfi1flim  25882  mbfmullem2  25883  itg2seq  25901  itg2uba  25902  itg2splitlem  25907  itg2monolem1  25909  itg2monolem2  25910  itg2monolem3  25911  itg2mono  25912  itg2i1fseqle  25913  itg2i1fseq  25914  itg2i1fseq2  25915  itg2addlem  25917  itg2cnlem1  25920  itg2cn  25922  limccnp2  26051  dvnff  26082  dvnp1  26084  cpnfval  26091  elcpn  26093  dvrec  26114  dvcnvlem  26135  dveflem  26138  dvef  26139  dvferm1  26144  dvferm2  26146  rolle  26149  dvlip  26152  dvlipcn  26153  dv11cn  26160  dvivthlem1  26167  dvivth  26169  lhop1lem  26172  ftc1lem1  26194  ftc1lem5  26199  ftc2  26203  itgsubstlem  26207  tdeglem3  26216  tdeglem4  26217  mdegval  26220  mdegmullem  26235  deg1fval  26237  deg1ldg  26249  deg1leb  26252  coe1mul3  26256  uc1pval  26297  mon1pval  26299  mon1pid  26311  q1pval  26312  r1pval  26315  ply1remlem  26322  ig1pval  26333  plyval  26350  elply2  26353  plyeq0lem  26367  coeval  26380  dgrval  26385  coeid2  26396  coemullem  26407  coemul  26409  plymulidp  26443  elqaalem1  26480  elqaalem2  26481  elqaalem3  26482  iaa  26488  aareccl  26489  aannenlem1  26491  geolim3  26502  aaliou3lem1  26505  aaliou3lem2  26506  aaliou3lem5  26510  aaliou3lem6  26511  aaliou3lem7  26512  aaliou3  26514  aaliou3r  26515  tayl0  26525  taylthlem1  26536  taylthlem2  26537  ulmshftlem  26552  ulmshft  26553  ulmuni  26555  ulmcau  26558  ulmdvlem1  26563  ulmdvlem3  26565  mtest  26567  mtestbdd  26568  mbfulm  26569  iblulm  26570  itgulm  26571  pserval  26573  pserval2  26574  radcnvlem1  26576  radcnvlem2  26577  dvradcnv  26584  pserulm  26585  pserdvlem2  26591  pserdv  26592  abelthlem1  26594  abelthlem3  26596  abelthlem4  26597  abelthlem5  26598  abelthlem6  26599  abelthlem7  26601  abelthlem8  26602  abelthlem9  26603  resinf1o  26701  efif1olem4  26710  eff1olem  26713  logcnlem5  26811  logtayllem  26824  logtayl  26825  logtaylsum  26826  logtayl2  26827  logccv  26828  asinval  27047  acosval  27048  atanval  27049  atantayl  27102  leibpilem2  27106  leibpi  27107  leibpisum  27108  log2cnv  27109  log2tlbnd  27110  areaval  27129  efrlim  27134  dfef2  27135  amgmlem  27154  emcllem2  27161  emcllem3  27162  emcllem4  27163  emcllem5  27164  emcllem6  27165  emcllem7  27166  zetacvg  27179  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulm2  27200  lgamcvglem  27204  igamval  27211  lgamcvg2  27219  gamcvg2lem  27223  ftalem7  27243  basellem2  27246  basellem3  27247  basellem4  27248  basellem5  27249  basellem6  27250  basellem8  27252  basellem9  27253  chtval  27274  vmaval  27277  chpval  27286  ppival  27291  muval  27296  prmorcht  27342  sqff1o  27346  dvdsflsumcom  27352  musum  27355  muinv  27357  sgmppw  27361  fsumvma  27377  pclogsum  27379  dchrfi  27419  bposlem5  27452  bposlem7  27454  bposlem8  27455  bposlem9  27456  lgsfval  27466  lgsdir  27496  lgsdilem2  27497  lgsdi  27498  lgsne0  27499  lgsqrlem2  27511  lgsqrlem4  27513  lgseisenlem2  27540  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasumiflem1  27665  dchrvmaeq0  27668  dchrisum0fval  27669  dchrisum0re  27677  mulog2sumlem1  27698  pntrval  27726  pntsval  27736  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntlem3  27773  abvcxp  27779  padicfval  27780  padicval  27781  padicabv  27794  ostth1  27797  ostth2  27801  ostth3  27802  nosupfv  27870  noinffv  27885  newval  28028  leftval  28042  rightval  28043  iscgrg  28781  legval  28853  ishpg  29041  iscgra  29120  isinag  29155  isleag  29164  iseqlg  29184  ttgval  29224  elee  29243  axsegconlem1  29267  axsegconlem9  29275  axsegconlem10  29276  axpasch  29291  axlowdimlem15  29306  axlowdim  29311  axeuclidlem  29312  axcontlem2  29315  eengv  29329  vtxval  29350  iedgval  29351  edgval  29399  vtxdgval  29818  wwlksnextinj  30248  wwlksnextsurj  30249  clwwlkfv  30399  clwwlknonmpo  30440  fusgreg2wsplem  30684  fusgreghash2wsp  30689  numclwwlk1lem2fv  30707  gidval  30864  grpoinvval  30875  bafval  30956  imsval  31037  dipfval  31054  sspval  31075  nmooval  31115  hmoval  31162  ipasslem8  31189  ipasslem9  31190  ipblnfi  31207  ubthlem2  31223  htthlem  31269  normval  31476  ocval  31632  occllem  31655  hsupval  31686  pjhfval  31748  pjhval  31749  chscllem2  31990  chscllem3  31991  hosval  32092  homval  32093  hodval  32094  hfsval  32095  hfmval  32096  brafval  32295  braval  32296  kbval  32306  eigvalval  32312  cnlnadjlem1  32419  nmopadjlei  32440  hmopidmchi  32503  strlem2  32603  hstrlem2  32611  cdj3lem2  32787  ofpreima  33010  psgnfzto1stlem  33420  evpmval  33465  altgnsg  33469  inftmrel  33500  isinftm  33501  qusker  33669  qusvscpbl  33671  qusvsval  33672  mxidlval  33744  idlsrgval  33793  psrmonmul  33940  dimval  33991  dimvalfi  33992  smatfval  34185  lmatval  34203  locfinreflem  34230  rspecval  34254  rmulccn  34318  xrmulc1cn  34320  xrge0iifcv  34324  xrge0iifiso  34325  xrge0iifhom  34327  xrge0iif1  34328  qqhval  34362  rrhval  34386  xrhval  34408  ddeval1  34624  ddeval0  34625  sxbrsigalem0  34661  sxbrsigalem3  34662  eulerpartlemgv  34763  rrvmbfm  34832  dstrvval  34861  coinflippv  34874  ballotlem2  34879  ballotlemfval  34880  ballotlemi  34891  ballotlemsval  34899  ballotlemrval  34908  ballotth  34928  signstfv  34950  signsvvfval  34965  kardval  35565  kard0  35567  onvf1odlem3  35589  derangval  35659  subfacval  35665  erdszelem3  35685  erdszelem9  35691  erdszelem10  35692  txpconn  35724  indispconn  35726  cvxpconn  35734  cvmlift2lem2  35796  cvmlift2lem3  35797  cvmlift2lem7  35801  cvmliftphtlem  35809  cvmlift3lem4  35814  snmlfval  35822  snmlval  35823  gonafv  35842  mvtval  35992  mrsubffval  35999  mrsubcv  36002  mrsubrn  36005  elmrsubrn  36012  msubffval  36015  mvhval  36026  mpstval  36027  mstaval  36036  mclsval  36055  mppsval  36064  sinccvglem  36164  circum  36166  divcnvlin  36225  iprodefisum  36233  iprodgam  36234  faclimlem1  36235  faclimlem2  36236  faclim  36238  iprodfac  36239  faclim2  36240  dfrdg2  36285  findabrcl  36965  dnival  37060  bj-evalval  37717  bj-inftyexpitaudisj  37849  bj-inftyexpiinv  37852  bj-inftyexpidisj  37854  curfv  38251  finixpnum  38256  poimirlem16  38287  poimir  38304  broucube  38305  mblfinlem2  38309  voliunnfl  38315  volsupnfl  38316  itg2addnclem  38322  itg2addnclem3  38324  ftc1cnnc  38343  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anc  38352  ftc2nc  38353  fvopabf4g  38373  sdclem2  38393  fdc  38396  lmclim2  38409  geomcau  38410  istotbnd  38420  isbnd  38431  prdsbnd2  38446  heiborlem6  38467  heiborlem7  38468  heiborlem8  38469  rrnval  38478  rrncmslem  38483  idlval  38664  pridlval  38684  maxidlval  38690  lshpset  39752  lsatset  39764  lcvfbr  39794  lflset  39833  lflnegcl  39849  lshpkrlem1  39884  lshpkrlem2  39885  lshpkrlem3  39886  ldualset  39899  cmtfvalN  39984  cvrfval  40042  pats  40059  llnset  40279  lplnset  40303  lvolset  40346  lineset  40512  pointsetN  40515  psubspset  40518  pmapval  40531  paddfval  40571  pclfvalN  40663  polfvalN  40678  polvalN  40679  psubclsetN  40710  watvalN  40767  lhpset  40769  lautset  40856  pautsetN  40872  ldilset  40883  ltrnset  40892  dilsetN  40927  trnsetN  40930  trlset  40935  trlval  40936  tgrpset  41519  tendoset  41533  tendo02  41561  erngset  41574  erngset-rN  41582  cdlemksv  41618  dvaset  41779  dvaplusgv  41784  diafval  41805  diaval  41806  dvhset  41855  cdlemm10N  41892  docafvalN  41896  djafvalN  41908  dibfval  41915  dibval  41916  dicfval  41949  dicval  41950  dihval  42006  dochfval  42124  djhfval  42171  dochfl1  42250  lpolsetN  42256  lcdval  42363  mapdhval  42498  hvmapfval  42533  hdmap1fval  42570  fimgmcyc  43302  prjspval  43335  isnacs  43435  mzpclval  43456  mzpsubst  43479  mzprename  43480  mzpcompact2lem  43482  eldiophb  43488  diophrw  43490  eldioph2  43493  diophin  43503  diophun  43504  diophren  43540  pell1qrval  43573  pell14qrval  43575  pell1234qrval  43577  pellfundval  43607  rmxypairf1o  43638  rmxyval  43642  mzpcong  43699  pw2f1ocnv  43764  dnnumch1  43771  dfac11  43789  hbtlem1  43850  hbtlem7  43852  elmnc  43863  dgraaval  43871  mpaaval  43878  itgoval  43888  flcidc  43897  mendval  43906  cytpval  43929  cantnfub  44048  cantnfresb  44051  tfsconcatrev  44075  elcnvlem  44327  comptiunov2i  44432  dftrcl3  44446  trclfvcom  44449  cnvtrclfv  44450  cotrcltrcl  44451  trclimalb2  44452  trclfvdecomr  44454  dfrtrcl3  44459  dfrtrcl4  44464  clsk1indlem0  44767  clsk1indlem2  44768  clsk1indlem3  44769  clsk1indlem4  44770  clsk1indlem1  44771  k0004val  44876  lhe4.4ex1a  45039  addrfv  45177  subrfv  45178  mulvfv  45179  monoord2xrv  46197  sumnnodd  46346  liminfgval  46476  ioodvbdlimc2lem  46648  itgsin0pilem1  46664  stoweidlem55  46769  wallispilem1  46779  wallispilem2  46780  wallispilem4  46782  wallispi2lem1  46785  wallispi2lem2  46786  dirkerval  46805  fourierdlem2  46823  fourierdlem3  46824  fourierdlem29  46850  fourierdlem62  46882  fourierdlem80  46900  fourierdlem103  46923  fourierdlem104  46924  fourierswlem  46944  fouriersw  46945  iundjiunlem  47173  carageniuncllem2  47236  0ome  47243  hoidmv1le  47308  hoidmvlelem3  47311  smflimsuplem7  47540  sqrtnnaa  47604  sqrtnzqaa  47605  iccpval  48164  fppr  48491  bigoval  49329  ackval0  49460  ackval41a  49474  eenglngeehlnm  49519  oppcinito  50013  oppctermo  50014  dfinito4  50279  prstcval  50329  mndtcval  50357  setc1onsubc  50380  lmdfval2  50433  cmdfval2  50434  vsetrec  50481  onsetreclem1  50483  elpglem3  50491  pgindnf  50494  sinhval-named  50514  coshval-named  50515  tanhval-named  50516  secval  50525  cscval  50526  cotval  50527  aacllem  50621