Theorem fvmpt 6991

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  fvmptex  7006  fvmptrabfv  7024  mptfvmpt  7232  fvmptopab  7473  ofval  7702  caofinvl  7723  fvresex  7970  1stval  8001  2ndval  8002  reldm  8053  curry1val  8114  curry2val  8118  fsplitfpar  8127  fnwelem  8141  brtpos2  8242  onovuni  8343  tz7.44-1  8407  oasuc  8525  oesuclem  8526  omsuc  8527  onasuc  8529  onmsuc  8530  fsetfocdm  8876  curfv  8885  fvmptmap  8902  xpcomco  9079  unxpdomlem1  9240  unfilem2  9291  ordtypelem3  9507  ixpiunwdom  9577  inf3lema  9618  noinfep  9654  cantnfval  9662  cantnflem1d  9682  cantnflem1  9683  ssttrcl  9709  ttrcltr  9710  ttrclselem2  9720  r1sucg  9769  r0weon  10084  infxpenc2lem1  10091  fseqenlem1  10096  fseqenlem2  10097  dfac8alem  10101  ac5num  10108  acni2  10118  dfac4  10194  dfac2a  10201  dfacacn  10213  dfac12lem1  10215  ackbij1lem7  10296  ackbij2lem2  10310  ackbij2lem3  10311  cfsmolem  10341  fin23lem28  10411  fin23lem39  10421  isf32lem6  10429  isf32lem7  10430  isf32lem8  10431  fin1a2lem3  10473  itunifval  10487  itunisuc  10490  axdc2lem  10519  axdc3lem2  10522  axcclem  10528  zorn2lem1  10567  negiso  12290  infrenegsup  12293  uzval  12960  flval  13927  ceilval  13971  ceilval2  13973  monoord2  14169  seqf1olem2  14178  seqf1o  14179  seqdistr  14189  serle  14193  seqof  14195  swrdfv  14789  revval  14902  revfv  14905  wwlktovf1  15103  wwlktovfo  15104  sgnval  15234  cjval  15262  reval  15266  imval  15267  sqrtval  15397  absval  15398  limsupval  15634  limsupgval  15636  climmpt  15731  climle  15800  rlimdiv  15806  isercolllem1  15825  isercoll2  15829  caurcvg2  15838  fsumser  15889  isumadd  15926  fsumcnv  15932  fsumrev  15938  fsumshft  15939  iserabs  15975  cvgcmp  15976  cvgcmpce  15978  incexclem  15998  isumless  16007  divcnvshft  16017  supcvg  16018  harmonic  16021  trireciplem  16024  trirecip  16025  expcnv  16026  explecnv  16027  geolim  16032  geolim2  16033  geo2lim  16037  geomulcvg  16038  geoisum  16039  geoisumr  16040  geoisum1  16041  geoisum1c  16042  cvgrat  16045  mertenslem2  16047  mertens  16048  prodfdiv  16058  fprodser  16109  fprodshft  16136  fprodrev  16137  fprodcnv  16143  iprodmul  16163  bpolylem  16207  eftval  16235  efval  16238  efcvgfsum  16245  ege2le3  16249  eftlub  16270  eflegeo  16282  sinval  16283  cosval  16284  tanval  16289  eirrlem  16365  rpnnen2lem1  16375  rpnnen2lem2  16376  bitsfval  16586  bitsinv2  16606  bitsinv  16611  sadcf  16616  sadc0  16617  sadcp1  16618  smupf  16641  smup0  16642  smupp1  16643  qnumval  16906  qdenval  16907  phival  16937  crth  16948  phimullem  16949  eulerthlem2  16952  phisum  16961  odzval  16962  iserodd  17006  pcmpt  17063  prmreclem1  17087  prmreclem2  17088  prmreclem4  17090  prmreclem5  17091  prmreclem6  17092  1arithlem1  17094  1arithlem2  17095  vdwapfval  17142  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  vdwlem9  17160  ramub1lem2  17198  ramcl  17200  prmoval  17204  strfvnd  17356  topnval  17598  prdsplusgfval  17638  prdsmulrfval  17640  isacs  17818  acsfn  17826  homffval  17857  comfffval  17865  oppcval  17880  monfval  17900  oppcmon  17906  sectffval  17918  invffval  17926  isoval  17933  idfuval  18044  homafval  18197  arwval  18211  coafval  18232  yonedainv  18448  oduval  18455  pltfval  18496  lubfval  18515  lubval  18521  glbfval  18528  glbval  18534  p0val  18592  p1val  18593  ipoval  18697  plusffval  18815  grpidval  18833  issubmgm  18884  issubm  18991  prdspjmhm  19018  efmnd  19059  smndex1gbas  19091  smndex1gid  19093  smndex1igid  19095  smndex1igidOLD  19096  grpinvfval  19182  grpinvval  19184  grpsubfval  19187  grpsubfvalALT  19188  grplactval  19245  prdsinvlem  19252  mulgfval  19272  mulgfvalALT  19273  pwsmulg  19322  issubg  19329  isnsg  19358  cycsubmel  19408  cycsubgcl  19414  conjghm  19456  conjnmz  19459  cntrval  19526  cntzfval  19527  cntzval  19528  oppgval  19554  psgnfval  19707  psgnval  19714  odfval  19739  odval  19741  sylow1lem4  19808  pgpssslw  19821  sylow2blem3  19829  sylow3lem2  19835  lsmfval  19845  pj1fval  19901  efgval  19924  efgsval  19938  frgpval  19965  vrgpval  19974  mulgmhm  20034  mulgghm  20035  ablfaclem1  20294  mgpval  20356  srglmhm  20440  srgrmhm  20441  ringlghm  20536  ringrghm  20537  pwspjmhmmgpd  20550  pwsexpg  20551  opprval  20561  dvdsrval  20584  isunit  20596  invrfval  20612  dvrfval  20625  isirred  20642  issubrng  20792  issubrg  20816  rgspnval  20857  rrgval  20942  fidomndrnglem  21023  issdrg  21038  abvfval  21060  abvtrivd  21082  staffval  21091  stafval  21092  scaffval  21148  lmodvsghm  21191  lssset  21201  lspfval  21241  islbs  21344  sraval  21443  rlmval  21459  2idlval  21537  lpival  21641  expmhm  21735  expghm  21774  mulgghm2  21775  mulgrhm  21776  zrhval  21806  zrhmulg  21808  zlmval  21814  chrval  21822  znval  21834  znzrhval  21845  evpmss  21885  psgnevpmb  21886  ip0l  21935  ipffval  21947  ocvfval  21965  ocvval  21966  cssval  21981  thlval  21994  pjfval  22005  pjval  22009  isobs  22019  prdsinvgd2  22041  uvcresum  22092  frlmup1  22097  frlmup2  22098  islinds  22108  islindf5  22138  aspval  22173  asclval  22180  psrmulval  22245  psrlidm  22262  psrridm  22263  psrascl  22279  mvrval  22282  mvrval2  22283  mplmonmul  22338  evlslem3  22382  evlslem1  22384  evlsval  22388  evlssca  22396  evlsvar  22397  psdmul  22480  psdmvr  22483  psr1val  22497  vr1val  22503  ply1val  22505  coe1fval  22516  coe1fv  22517  coe1tmmul2  22588  coe1tmmul  22589  coe1tmmul2fv  22590  coe1pwmulfv  22592  evls1val  22631  evl1fval  22639  evl1val  22640  mamulid  22749  mamurid  22750  mdetleib  22895  mdetleib1  22899  mdetunilem9  22928  mdetuni0  22929  mdetmul  22931  cpmidpmatlem1  23181  ordtval  23500  cnpval  23547  ptpjpre1  23883  ptpjopn  23924  dfac14  23930  upxp  23935  uptx  23937  hauseqlcld  23958  txlm  23960  xkoptsub  23966  xkoinjcn  23999  kqval  24038  xpstopnlem1  24121  fmval  24255  flfval  24302  ptcmplem2  24365  ptcmplem3  24366  symgtgp  24418  qustgpopn  24432  ussval  24571  iscfilu  24599  ispsmet  24616  ismet  24635  isxmet  24636  mopnval  24750  prdsxmslem2  24841  nmfval  24900  nmval  24901  nmoval  25027  metdsval  25160  divcn  25182  mulc1cncf  25219  icopnfhmeo  25257  iccpnfhmeo  25259  xrhmeo  25260  cnheiborlem  25268  evth  25273  evth2  25274  lebnumlem3  25277  isphtpy  25295  isphtpc  25308  pcofval  25324  pcovalg  25326  pco1  25329  pcopt  25336  pcopt2  25337  pcoass  25338  pcorevcl  25339  pcorevlem  25340  pcorev2  25342  pi1xfrcnv  25371  cphnm  25507  tcphval  25532  tcphnmval  25543  cfilfval  25578  iscmet  25598  iscmet3lem3  25604  rrxval  25701  ehlval  25728  ivth2  25769  ovolval  25787  ovollb2lem  25802  ovolunlem1a  25810  ovolunlem1  25811  ovoliunlem1  25816  ovoliunlem2  25817  ovolicc1  25830  voliunlem1  25864  voliunlem2  25865  voliunlem3  25866  volsup  25870  ioorval  25888  uniioombllem3  25899  uniioombllem6  25902  volsup2  25919  volcn  25920  volivth  25921  vitalilem2  25923  vitalilem3  25924  vitalilem4  25925  vitali  25927  mbfmax  25963  mbfimaopnlem  25969  itg1val  25997  i1f1lem  26003  itg11  26005  itg1addlem4  26013  itg1mulc  26018  i1fres  26019  itg1climres  26028  mbfi1fseqlem2  26030  mbfi1fseqlem3  26031  mbfi1fseqlem6  26034  mbfi1flimlem  26036  mbfi1flim  26037  mbfmullem2  26038  itg2seq  26056  itg2uba  26057  itg2splitlem  26062  itg2monolem1  26064  itg2monolem2  26065  itg2monolem3  26066  itg2mono  26067  itg2i1fseqle  26068  itg2i1fseq  26069  itg2i1fseq2  26070  itg2addlem  26072  itg2cnlem1  26075  itg2cn  26077  limccnp2  26205  dvnff  26236  dvnp1  26238  cpnfval  26245  elcpn  26247  dvrec  26268  dvcnvlem  26289  dveflem  26292  dvef  26293  dvferm1  26298  dvferm2  26300  rolle  26303  dvlip  26306  dvlipcn  26307  dv11cn  26314  dvivthlem1  26321  dvivth  26323  lhop1lem  26326  ftc1lem1  26348  ftc1lem5  26353  ftc2  26357  itgsubstlem  26361  tdeglem3  26370  tdeglem4  26371  mdegval  26374  mdegmullem  26389  deg1fval  26391  deg1ldg  26403  deg1leb  26406  coe1mul3  26410  uc1pval  26451  mon1pval  26453  mon1pid  26465  q1pval  26466  r1pval  26469  ply1remlem  26476  ig1pval  26487  plyval  26504  elply2  26507  plyeq0lem  26522  coeval  26535  dgrval  26540  coeid2  26551  coemullem  26562  coemul  26564  plymulidp  26596  elqaalem1  26635  elqaalem2  26636  elqaalem3  26637  iaa  26644  iaaOLD  26645  aareccl  26646  aannenlem1  26648  geolim3  26659  aaliou3lem1  26662  aaliou3lem2  26663  aaliou3lem5  26667  aaliou3lem6  26668  aaliou3lem7  26669  aaliou3  26671  aaliou3r  26672  tayl0  26682  taylthlem1  26693  taylthlem2  26694  ulmshftlem  26709  ulmshft  26710  ulmuni  26712  ulmcau  26715  ulmdvlem1  26720  ulmdvlem3  26722  mtest  26724  mtestbdd  26725  mbfulm  26726  iblulm  26727  itgulm  26728  pserval  26730  pserval2  26731  radcnvlem1  26733  radcnvlem2  26734  dvradcnv  26741  pserulm  26742  pserdvlem2  26748  pserdv  26749  abelthlem1  26751  abelthlem3  26753  abelthlem4  26754  abelthlem5  26755  abelthlem6  26756  abelthlem7  26758  abelthlem8  26759  abelthlem9  26760  resinf1o  26857  efif1olem4  26866  eff1olem  26869  logcnlem5  26967  logtayllem  26980  logtayl  26981  logtaylsum  26982  logtayl2  26983  logccv  26984  asinval  27203  acosval  27204  atanval  27205  atantayl  27258  leibpilem2  27262  leibpi  27263  leibpisum  27264  log2cnv  27265  log2tlbnd  27266  areaval  27285  efrlim  27290  dfef2  27291  amgmlem  27310  emcllem2  27317  emcllem3  27318  emcllem4  27319  emcllem5  27320  emcllem6  27321  emcllem7  27322  zetacvg  27335  lgamgulmlem4  27352  lgamgulmlem5  27353  lgamgulm2  27356  lgamcvglem  27360  igamval  27367  lgamcvg2  27375  gamcvg2lem  27379  ftalem7  27399  basellem2  27402  basellem3  27403  basellem4  27404  basellem5  27405  basellem6  27406  basellem8  27408  basellem9  27409  chtval  27430  vmaval  27433  chpval  27442  ppival  27447  muval  27452  prmorcht  27498  sqff1o  27502  dvdsflsumcom  27508  musum  27511  muinv  27513  sgmppw  27517  fsumvma  27533  pclogsum  27535  dchrfi  27575  bposlem5  27608  bposlem7  27610  bposlem8  27611  bposlem9  27612  lgsfval  27622  lgsdir  27652  lgsdilem2  27653  lgsdi  27654  lgsne0  27655  lgsqrlem2  27667  lgsqrlem4  27669  lgseisenlem2  27696  dchrmusum2  27814  dchrvmasumlem1  27815  dchrvmasumiflem1  27821  dchrvmaeq0  27824  dchrisum0fval  27825  dchrisum0re  27833  mulog2sumlem1  27854  pntrval  27882  pntsval  27892  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntlem3  27929  abvcxp  27935  padicfval  27936  padicval  27937  padicabv  27950  ostth1  27953  ostth2  27957  ostth3  27958  nosupfv  28056  noinffv  28071  newval  28214  leftval  28228  rightval  28229  iscgrg  28968  legval  29040  ishpg  29230  iscgra  29309  isinag  29350  isleag  29359  iseqlg  29405  ttgval  29445  elee  29464  axsegconlem1  29488  axsegconlem9  29496  axsegconlem10  29497  axpasch  29512  axlowdimlem15  29527  axlowdim  29532  axeuclidlem  29533  axcontlem2  29536  eengv  29550  vtxval  29571  iedgval  29572  edgval  29620  vtxdgval  30042  wwlksnextinj  30481  wwlksnextsurj  30482  clwwlkfv  30632  clwwlknonmpo  30673  fusgreg2wsplem  30927  fusgreghash2wsp  30932  numclwwlk1lem2fv  30950  gidval  31107  grpoinvval  31118  bafval  31199  imsval  31280  dipfval  31297  sspval  31318  nmooval  31358  hmoval  31405  ipasslem8  31432  ipasslem9  31433  ipblnfi  31450  ubthlem2  31466  htthlem  31512  normval  31719  ocval  31875  occllem  31898  hsupval  31929  pjhfval  31991  pjhval  31992  chscllem2  32233  chscllem3  32234  hosval  32335  homval  32336  hodval  32337  hfsval  32338  hfmval  32339  brafval  32538  braval  32539  kbval  32549  eigvalval  32555  cnlnadjlem1  32662  nmopadjlei  32683  hmopidmchi  32746  strlem2  32846  hstrlem2  32854  cdj3lem2  33030  ofpreima  33252  psgnfzto1stlem  33654  evpmval  33699  altgnsg  33703  inftmrel  33734  isinftm  33735  qusker  33903  qusvscpbl  33905  qusvsval  33906  mxidlval  33979  idlsrgval  34028  psrmonmul  34175  dimval  34226  dimvalfi  34227  smatfval  34420  lmatval  34438  locfinreflem  34465  rspecval  34489  rmulccn  34553  xrmulc1cn  34555  xrge0iifcv  34559  xrge0iifiso  34560  xrge0iifhom  34562  xrge0iif1  34563  qqhval  34597  rrhval  34621  xrhval  34643  ddeval1  34860  ddeval0  34861  sxbrsigalem0  34896  sxbrsigalem3  34897  eulerpartlemgv  34998  rrvmbfm  35067  dstrvval  35096  coinflippv  35109  ballotlem2  35114  ballotlemfval  35115  ballotlemi  35126  ballotlemsval  35134  ballotlemrval  35143  ballotth  35163  signstfv  35185  signsvvfval  35200  kardval  35803  kard0  35805  onvf1odlem3  35867  derangval  35911  subfacval  35917  erdszelem3  35937  erdszelem9  35943  erdszelem10  35944  txpconn  35976  indispconn  35978  cvxpconn  35986  cvmlift2lem2  36048  cvmlift2lem3  36049  cvmlift2lem7  36053  cvmliftphtlem  36061  cvmlift3lem4  36066  snmlfval  36074  snmlval  36075  gonafv  36094  mvtval  36244  mrsubffval  36251  mrsubcv  36254  mrsubrn  36257  elmrsubrn  36264  msubffval  36267  mvhval  36278  mpstval  36279  mstaval  36288  mclsval  36307  mppsval  36316  sinccvglem  36416  circum  36418  divcnvlin  36477  iprodefisum  36485  iprodgam  36486  faclimlem1  36487  faclimlem2  36488  faclim  36490  iprodfac  36491  faclim2  36492  dfrdg2  36537  findabrcl  37222  dnival  37317  bj-evalval  37976  bj-inftyexpitaudisj  38106  bj-inftyexpiinv  38109  bj-inftyexpidisj  38111  finixpnum  38508  poimirlem16  38534  poimir  38551  broucube  38552  mblfinlem2  38556  voliunnfl  38562  volsupnfl  38563  itg2addnclem  38569  itg2addnclem3  38571  ftc1cnnc  38590  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anc  38599  ftc2nc  38600  varprop  38622  negprop  38623  impprop  38624  dfprop2  38626  fvopabf4g  38636  sdclem2  38656  fdc  38659  lmclim2  38672  geomcau  38673  istotbnd  38683  isbnd  38694  prdsbnd2  38709  heiborlem6  38730  heiborlem7  38731  heiborlem8  38732  rrnval  38741  rrncmslem  38746  idlval  38927  pridlval  38947  maxidlval  38953  lshpset  40015  lsatset  40027  lcvfbr  40057  lflset  40096  lflnegcl  40112  lshpkrlem1  40147  lshpkrlem2  40148  lshpkrlem3  40149  ldualset  40162  cmtfvalN  40247  cvrfval  40305  pats  40322  llnset  40542  lplnset  40566  lvolset  40609  lineset  40775  pointsetN  40778  psubspset  40781  pmapval  40794  paddfval  40834  pclfvalN  40926  polfvalN  40941  polvalN  40942  psubclsetN  40973  watvalN  41030  lhpset  41032  lautset  41119  pautsetN  41135  ldilset  41146  ltrnset  41155  dilsetN  41190  trnsetN  41193  trlset  41198  trlval  41199  tgrpset  41782  tendoset  41796  tendo02  41824  erngset  41837  erngset-rN  41845  cdlemksv  41881  dvaset  42042  dvaplusgv  42047  diafval  42068  diaval  42069  dvhset  42118  cdlemm10N  42155  docafvalN  42159  djafvalN  42171  dibfval  42178  dibval  42179  dicfval  42212  dicval  42213  dihval  42269  dochfval  42387  djhfval  42434  dochfl1  42513  lpolsetN  42519  lcdval  42626  mapdhval  42761  hvmapfval  42796  hdmap1fval  42833  fimgmcyc  43578  prjspval  43611  isnacs  43694  mzpclval  43715  mzpsubst  43738  mzprename  43739  mzpcompact2lem  43741  eldiophb  43747  diophrw  43749  eldioph2  43752  diophin  43762  diophun  43763  diophren  43799  pell1qrval  43832  pell14qrval  43834  pell1234qrval  43836  pellfundval  43866  rmxypairf1o  43897  rmxyval  43901  mzpcong  43958  pw2f1ocnv  44023  dnnumch1  44030  dfac11  44048  hbtlem1  44109  hbtlem7  44111  elmnc  44122  dgraaval  44130  mpaaval  44137  itgoval  44147  flcidc  44156  mendval  44165  cytpval  44188  cantnfub  44307  cantnfresb  44310  tfsconcatrev  44334  elcnvlem  44586  comptiunov2i  44691  dftrcl3  44705  trclfvcom  44708  cnvtrclfv  44709  cotrcltrcl  44710  trclimalb2  44711  trclfvdecomr  44713  dfrtrcl3  44718  dfrtrcl4  44723  clsk1indlem0  45026  clsk1indlem2  45027  clsk1indlem3  45028  clsk1indlem4  45029  clsk1indlem1  45030  k0004val  45135  lhe4.4ex1a  45298  addrfv  45436  subrfv  45437  mulvfv  45438  monoord2xrv  46462  sumnnodd  46611  liminfgval  46741  ioodvbdlimc2lem  46913  itgsin0pilem1  46929  stoweidlem55  47034  wallispilem1  47044  wallispilem2  47045  wallispilem4  47047  wallispi2lem1  47050  wallispi2lem2  47051  dirkerval  47070  fourierdlem2  47088  fourierdlem3  47089  fourierdlem29  47115  fourierdlem62  47147  fourierdlem80  47165  fourierdlem103  47188  fourierdlem104  47189  fourierswlem  47209  fouriersw  47210  iundjiunlem  47438  carageniuncllem2  47501  0ome  47508  hoidmv1le  47573  hoidmvlelem3  47576  smflimsuplem7  47805  sqrtnnaa  47882  sqrtnzqaa  47883  sqrtnpoly  47912  iccpval  48466  fppr  48793  bigoval  49630  ackval0  49761  ackval41a  49775  eenglngeehlnm  49820  oppcinito  50312  oppctermo  50313  dfinito4  50578  prstcval  50628  mndtcval  50656  setc1onsubc  50679  lmdfval2  50732  cmdfval2  50733  vsetrec  50765  onsetreclem1  50767  elpglem3  50775  pgindnf  50778  sinhval-named  50798  coshval-named  50799  tanhval-named  50800  secval  50809  cscval  50810  cotval  50811  aacllem  50908