Theorem fvmpt 7024

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5192  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574

This theorem is used by:  fvmptex  7039  fvmptrabfv  7057  mptfvmpt  7265  fvmptopab  7506  ofval  7736  caofinvl  7757  fvresex  8006  1stval  8037  2ndval  8038  reldmOLD  8090  curry1val  8153  curry2val  8157  fsplitfpar  8166  fnwelem  8180  brtpos2  8287  onovuni  8388  tz7.44-1  8452  oasuc  8570  oesuclem  8571  omsuc  8572  onasuc  8574  onmsuc  8575  fsetfocdm  8921  curfv  8930  fvmptmap  8947  xpcomco  9124  unxpdomlem1  9285  unfilem2  9336  ordtypelem3  9551  ixpiunwdom  9621  inf3lema  9662  noinfep  9698  cantnfval  9706  cantnflem1d  9726  cantnflem1  9727  ssttrcl  9753  ttrcltr  9754  ttrclselem2  9764  r1sucg  9813  r0weon  10130  infxpenc2lem1  10137  fseqenlem1  10142  fseqenlem2  10143  dfac8alem  10147  ac5num  10154  acni2  10164  dfac4  10240  dfac2a  10247  dfacacn  10259  dfac12lem1  10261  ackbij1lem7  10342  ackbij2lem2  10356  ackbij2lem3  10357  cfsmolem  10387  fin23lem28  10457  fin23lem39  10467  isf32lem6  10475  isf32lem7  10476  isf32lem8  10477  fin1a2lem3  10519  itunifval  10533  itunisuc  10536  axdc2lem  10565  axdc3lem2  10568  axcclem  10574  zorn2lem1  10613  negiso  12337  infrenegsup  12340  uzval  13007  flval  13974  ceilval  14018  ceilval2  14020  monoord2  14216  seqf1olem2  14225  seqf1o  14226  seqdistr  14236  serle  14240  seqof  14242  swrdfv  14838  revval  14951  revfv  14954  wwlktovf1  15153  wwlktovfo  15154  sgnval  15284  cjval  15312  reval  15316  imval  15317  sqrtval  15447  absval  15448  limsupval  15685  limsupgval  15687  climmpt  15782  climle  15851  rlimdiv  15857  isercolllem1  15876  isercoll2  15880  caurcvg2  15889  fsumser  15940  isumadd  15977  fsumcnv  15983  fsumrev  15989  fsumshft  15990  iserabs  16026  cvgcmp  16027  cvgcmpce  16029  incexclem  16049  isumless  16058  divcnvshft  16068  supcvg  16069  harmonic  16072  trireciplem  16075  trirecip  16076  expcnv  16077  explecnv  16078  geolim  16083  geolim2  16084  geo2lim  16088  geomulcvg  16089  geoisum  16090  geoisumr  16091  geoisum1  16092  geoisum1c  16093  cvgrat  16096  mertenslem2  16098  mertens  16099  prodfdiv  16109  fprodser  16160  fprodshft  16187  fprodrev  16188  fprodcnv  16194  iprodmul  16214  bpolylem  16258  eftval  16286  efval  16289  efcvgfsum  16296  ege2le3  16300  eftlub  16321  eflegeo  16333  sinval  16334  cosval  16335  tanval  16340  eirrlem  16416  rpnnen2lem1  16426  rpnnen2lem2  16427  bitsfval  16637  bitsinv2  16657  bitsinv  16662  sadcf  16667  sadc0  16668  sadcp1  16669  smupf  16692  smup0  16693  smupp1  16694  qnumval  16957  qdenval  16958  phival  16988  crth  16999  phimullem  17000  eulerthlem2  17003  phisum  17012  odzval  17013  iserodd  17057  pcmpt  17114  prmreclem1  17138  prmreclem2  17139  prmreclem4  17141  prmreclem5  17142  prmreclem6  17143  1arithlem1  17145  1arithlem2  17146  vdwapfval  17193  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  vdwlem9  17211  ramub1lem2  17249  ramcl  17251  prmoval  17255  strfvnd  17407  topnval  17655  prdsplusgfval  17695  prdsmulrfval  17697  isacs  17875  acsfn  17883  homffval  17914  comfffval  17922  oppcval  17937  monfval  17957  oppcmon  17963  sectffval  17975  invffval  17983  isoval  17990  idfuval  18101  homafval  18254  arwval  18268  coafval  18289  yonedainv  18505  oduval  18512  pltfval  18553  lubfval  18572  lubval  18578  glbfval  18585  glbval  18591  p0val  18649  p1val  18650  ipoval  18754  plusffval  18872  grpidval  18890  issubmgm  18941  issubm  19048  prdspjmhm  19075  efmnd  19116  smndex1gbas  19148  smndex1gid  19150  smndex1igid  19152  smndex1igidOLD  19153  grpinvfval  19239  grpinvval  19241  grpsubfval  19244  grpsubfvalALT  19245  grplactval  19302  prdsinvlem  19309  mulgfval  19329  mulgfvalALT  19330  pwsmulg  19379  issubg  19386  isnsg  19415  cycsubmel  19465  cycsubgcl  19471  conjghm  19513  conjnmz  19516  cntrval  19584  cntzfval  19585  cntzval  19586  oppgval  19612  psgnfval  19765  psgnval  19772  odfval  19797  odval  19799  sylow1lem4  19866  pgpssslw  19879  sylow2blem3  19887  sylow3lem2  19893  lsmfval  19903  pj1fval  19959  efgval  19982  efgsval  19996  frgpval  20023  vrgpval  20032  mulgmhm  20092  mulgghm  20093  ablfaclem1  20352  mgpval  20414  srglmhm  20498  srgrmhm  20499  ringlghm  20594  ringrghm  20595  pwspjmhmmgpd  20608  pwsexpg  20609  opprval  20619  dvdsrval  20642  isunit  20654  invrfval  20670  dvrfval  20683  isirred  20700  issubrng  20850  issubrg  20874  rgspnval  20915  rrgval  21000  fidomndrnglem  21081  issdrg  21096  abvfval  21118  abvtrivd  21140  staffval  21149  stafval  21150  scaffval  21206  lmodvsghm  21249  lssset  21259  lspfval  21299  islbs  21402  sraval  21501  rlmval  21517  2idlval  21595  lpival  21699  expmhm  21796  expghm  21836  mulgghm2  21837  mulgrhm  21838  zrhval  21868  zrhmulg  21870  zlmval  21876  chrval  21884  znval  21896  znzrhval  21907  evpmss  21947  psgnevpmb  21948  ip0l  21997  ipffval  22009  ocvfval  22027  ocvval  22028  cssval  22043  thlval  22056  pjfval  22067  pjval  22071  isobs  22081  prdsinvgd2  22103  uvcresum  22154  frlmup1  22159  frlmup2  22160  islinds  22170  islindf5  22200  aspval  22235  asclval  22242  psrmulval  22307  psrlidm  22324  psrridm  22325  psrascl  22341  mvrval  22344  mvrval2  22345  mplmonmul  22400  evlslem3  22444  evlslem1  22446  evlsval  22450  evlssca  22458  evlsvar  22459  psdmul  22542  psdmvr  22545  psr1val  22559  vr1val  22565  ply1val  22567  coe1fval  22578  coe1fv  22579  coe1tmmul2  22650  coe1tmmul  22651  coe1tmmul2fv  22652  coe1pwmulfv  22654  evls1val  22693  evl1fval  22701  evl1val  22702  mamulid  22811  mamurid  22812  mdetleib  22957  mdetleib1  22961  mdetunilem9  22990  mdetuni0  22991  mdetmul  22993  cpmidpmatlem1  23243  ordtval  23562  cnpval  23609  ptpjpre1  23945  ptpjopn  23986  dfac14  23992  upxp  23997  uptx  23999  hauseqlcld  24020  txlm  24022  xkoptsub  24028  xkoinjcn  24061  kqval  24100  xpstopnlem1  24183  fmval  24317  flfval  24364  ptcmplem2  24427  ptcmplem3  24428  symgtgp  24480  qustgpopn  24494  ussval  24633  iscfilu  24661  ispsmet  24678  ismet  24697  isxmet  24698  mopnval  24812  prdsxmslem2  24903  nmfval  24962  nmval  24963  nmoval  25089  metdsval  25222  divcn  25244  mulc1cncf  25281  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  cnheiborlem  25330  evth  25335  evth2  25336  lebnumlem3  25339  isphtpy  25357  isphtpc  25370  pcofval  25386  pcovalg  25388  pco1  25391  pcopt  25398  pcopt2  25399  pcoass  25400  pcorevcl  25401  pcorevlem  25402  pcorev2  25404  pi1xfrcnv  25433  cphnm  25569  tcphval  25594  tcphnmval  25605  cfilfval  25640  iscmet  25660  iscmet3lem3  25666  rrxval  25763  ehlval  25790  ivth2  25831  ovolval  25849  ovollb2lem  25864  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliunlem2  25879  ovolicc1  25892  voliunlem1  25926  voliunlem2  25927  voliunlem3  25928  volsup  25932  ioorval  25950  uniioombllem3  25961  uniioombllem6  25964  volsup2  25981  volcn  25982  volivth  25983  vitalilem2  25985  vitalilem3  25986  vitalilem4  25987  vitali  25989  mbfmax  26025  mbfimaopnlem  26031  itg1val  26059  i1f1lem  26065  itg11  26067  itg1addlem4  26075  itg1mulc  26080  i1fres  26081  itg1climres  26090  mbfi1fseqlem2  26092  mbfi1fseqlem3  26093  mbfi1fseqlem6  26096  mbfi1flimlem  26098  mbfi1flim  26099  mbfmullem2  26100  itg2seq  26118  itg2uba  26119  itg2splitlem  26124  itg2monolem1  26126  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2i1fseqle  26130  itg2i1fseq  26131  itg2i1fseq2  26132  itg2addlem  26134  itg2cnlem1  26137  itg2cn  26139  limccnp2  26267  dvnff  26298  dvnp1  26300  cpnfval  26307  elcpn  26309  dvrec  26330  dvcnvlem  26351  dveflem  26354  dvef  26355  dvferm1  26360  dvferm2  26362  rolle  26365  dvlip  26368  dvlipcn  26369  dv11cn  26376  dvivthlem1  26383  dvivth  26385  lhop1lem  26388  ftc1lem1  26410  ftc1lem5  26415  ftc2  26419  itgsubstlem  26423  tdeglem3  26432  tdeglem4  26433  mdegval  26436  mdegmullem  26451  deg1fval  26453  deg1ldg  26465  deg1leb  26468  coe1mul3  26472  uc1pval  26513  mon1pval  26515  mon1pid  26527  q1pval  26528  r1pval  26531  ply1remlem  26538  ig1pval  26549  plyval  26566  elply2  26569  plyeq0lem  26584  coeval  26597  dgrval  26602  coeid2  26613  coemullem  26624  coemul  26626  plymulidp  26658  elqaalem1  26699  elqaalem2  26700  elqaalem3  26701  iaa  26708  iaaOLD  26709  aareccl  26710  aannenlem1  26712  geolim3  26723  aaliou3lem1  26726  aaliou3lem2  26727  aaliou3lem5  26731  aaliou3lem6  26732  aaliou3lem7  26733  aaliou3  26735  aaliou3r  26736  tayl0  26746  taylthlem1  26757  taylthlem2  26758  ulmshftlem  26773  ulmshft  26774  ulmuni  26776  ulmcau  26779  ulmdvlem1  26784  ulmdvlem3  26786  mtest  26788  mtestbdd  26789  mbfulm  26790  iblulm  26791  itgulm  26792  pserval  26794  pserval2  26795  radcnvlem1  26797  radcnvlem2  26798  dvradcnv  26805  pserulm  26806  pserdvlem2  26812  pserdv  26813  abelthlem1  26815  abelthlem3  26817  abelthlem4  26818  abelthlem5  26819  abelthlem6  26820  abelthlem7  26822  abelthlem8  26823  abelthlem9  26824  resinf1o  26921  efif1olem4  26930  eff1olem  26933  logcnlem5  27031  logtayllem  27044  logtayl  27045  logtaylsum  27046  logtayl2  27047  logccv  27048  asinval  27267  acosval  27268  atanval  27269  atantayl  27322  leibpilem2  27326  leibpi  27327  leibpisum  27328  log2cnv  27329  log2tlbnd  27330  areaval  27349  efrlim  27354  dfef2  27355  amgmlem  27374  emcllem2  27381  emcllem3  27382  emcllem4  27383  emcllem5  27384  emcllem6  27385  emcllem7  27386  zetacvg  27399  lgamgulmlem4  27416  lgamgulmlem5  27417  lgamgulm2  27420  lgamcvglem  27424  igamval  27431  lgamcvg2  27439  gamcvg2lem  27443  ftalem7  27463  basellem2  27466  basellem3  27467  basellem4  27468  basellem5  27469  basellem6  27470  basellem8  27472  basellem9  27473  chtval  27494  vmaval  27497  chpval  27506  ppival  27511  muval  27516  prmorcht  27562  sqff1o  27566  dvdsflsumcom  27572  musum  27575  muinv  27577  sgmppw  27581  fsumvma  27597  pclogsum  27599  dchrfi  27639  bposlem5  27672  bposlem7  27674  bposlem8  27675  bposlem9  27676  lgsfval  27686  lgsdir  27716  lgsdilem2  27717  lgsdi  27718  lgsne0  27719  lgsqrlem2  27731  lgsqrlem4  27733  lgseisenlem2  27760  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasumiflem1  27885  dchrvmaeq0  27888  dchrisum0fval  27889  dchrisum0re  27897  mulog2sumlem1  27918  pntrval  27946  pntsval  27956  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntlem3  27993  abvcxp  27999  padicfval  28000  padicval  28001  padicabv  28014  ostth1  28017  ostth2  28021  ostth3  28022  nosupfv  28120  noinffv  28135  newval  28278  leftval  28292  rightval  28293  iscgrg  29032  legval  29104  ishpg  29294  iscgra  29373  isinag  29414  isleag  29423  iseqlg  29469  ttgval  29509  elee  29528  axsegconlem1  29552  axsegconlem9  29560  axsegconlem10  29561  axpasch  29576  axlowdimlem15  29591  axlowdim  29596  axeuclidlem  29597  axcontlem2  29600  eengv  29614  vtxval  29635  iedgval  29636  edgval  29684  vtxdgval  30106  wwlksnextinj  30545  wwlksnextsurj  30546  clwwlkfv  30696  clwwlknonmpo  30737  fusgreg2wsplem  30991  fusgreghash2wsp  30996  numclwwlk1lem2fv  31014  gidval  31171  grpoinvval  31182  bafval  31263  imsval  31344  dipfval  31361  sspval  31382  nmooval  31422  hmoval  31469  ipasslem8  31496  ipasslem9  31497  ipblnfi  31514  ubthlem2  31530  htthlem  31576  normval  31783  ocval  31939  occllem  31962  hsupval  31993  pjhfval  32055  pjhval  32056  chscllem2  32297  chscllem3  32298  hosval  32399  homval  32400  hodval  32401  hfsval  32402  hfmval  32403  brafval  32602  braval  32603  kbval  32613  eigvalval  32619  cnlnadjlem1  32726  nmopadjlei  32747  hmopidmchi  32810  strlem2  32910  hstrlem2  32918  cdj3lem2  33094  ofpreima  33357  psgnfzto1stlem  33760  evpmval  33805  altgnsg  33809  inftmrel  33840  isinftm  33841  qusker  34014  qusvscpbl  34016  qusvsval  34017  mxidlval  34090  idlsrgval  34139  psrmonmul  34293  dimval  34344  dimvalfi  34345  smatfval  34538  lmatval  34556  locfinreflem  34583  rspecval  34607  rmulccn  34671  xrmulc1cn  34673  xrge0iifcv  34677  xrge0iifiso  34678  xrge0iifhom  34680  xrge0iif1  34681  qqhval  34715  rrhval  34739  xrhval  34761  ddeval1  34978  ddeval0  34979  sxbrsigalem0  35014  sxbrsigalem3  35015  eulerpartlemgv  35116  rrvmbfm  35185  dstrvval  35214  coinflippv  35227  ballotlem2  35232  ballotlemfval  35233  ballotlemi  35244  ballotlemsval  35252  ballotlemrval  35261  ballotth  35281  signstfv  35303  signsvvfval  35318  kardval  35961  kard0  35963  j00smo  36046  maxssj0  36047  k1on  36056  k2on  36057  k39o  36058  jk1k2k3  36059  onvf1odlem3  36074  derangval  36140  subfacval  36146  erdszelem3  36166  erdszelem9  36172  erdszelem10  36173  txpconn  36205  indispconn  36207  cvxpconn  36215  cvmlift2lem2  36277  cvmlift2lem3  36278  cvmlift2lem7  36282  cvmliftphtlem  36290  cvmlift3lem4  36295  snmlfval  36303  snmlval  36304  gonafv  36323  mvtval  36473  mrsubffval  36480  mrsubcv  36483  mrsubrn  36486  elmrsubrn  36493  msubffval  36496  mvhval  36507  mpstval  36508  mstaval  36517  mclsval  36536  mppsval  36545  sinccvglem  36645  circum  36647  mirimanoffr  36668  divcnvlin  36713  iprodefisum  36721  iprodgam  36722  faclimlem1  36723  faclimlem2  36724  faclim  36726  iprodfac  36727  faclim2  36728  dfrdg2  36772  findabrcl  37457  dnival  37552  bj-evalval  38266  bj-inftyexpitaudisj  38394  bj-inftyexpiinv  38397  bj-inftyexpidisj  38399  finixpnum  38796  poimirlem16  38822  poimir  38839  broucube  38840  mblfinlem2  38844  voliunnfl  38850  volsupnfl  38851  itg2addnclem  38857  itg2addnclem3  38859  ftc1cnnc  38878  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anc  38887  ftc2nc  38888  varprop  38910  negprop  38911  impprop  38912  dfprop2  38914  fvopabf4g  38924  sdclem2  38942  fdc  38945  lmclim2  38958  geomcau  38959  istotbnd  38969  isbnd  38980  prdsbnd2  38995  heiborlem6  39016  heiborlem7  39017  heiborlem8  39018  rrnval  39027  rrncmslem  39032  idlval  39213  pridlval  39233  maxidlval  39239  lshpset  40301  lsatset  40313  lcvfbr  40343  lflset  40382  lflnegcl  40398  lshpkrlem1  40433  lshpkrlem2  40434  lshpkrlem3  40435  ldualset  40448  cmtfvalN  40533  cvrfval  40591  pats  40608  llnset  40828  lplnset  40852  lvolset  40895  lineset  41061  pointsetN  41064  psubspset  41067  pmapval  41080  paddfval  41120  pclfvalN  41212  polfvalN  41227  polvalN  41228  psubclsetN  41259  watvalN  41316  lhpset  41318  lautset  41405  pautsetN  41421  ldilset  41432  ltrnset  41441  dilsetN  41476  trnsetN  41479  trlset  41484  trlval  41485  tgrpset  42068  tendoset  42082  tendo02  42110  erngset  42123  erngset-rN  42131  cdlemksv  42167  dvaset  42328  dvaplusgv  42333  diafval  42354  diaval  42355  dvhset  42404  cdlemm10N  42441  docafvalN  42445  djafvalN  42457  dibfval  42464  dibval  42465  dicfval  42498  dicval  42499  dihval  42555  dochfval  42673  djhfval  42720  dochfl1  42799  lpolsetN  42805  lcdval  42912  mapdhval  43047  hvmapfval  43082  hdmap1fval  43119  fimgmcyc  43864  prjspval  43897  isnacs  43981  mzpclval  44002  mzpsubst  44025  mzprename  44026  mzpcompact2lem  44028  eldiophb  44034  diophrw  44036  eldioph2  44039  diophin  44049  diophun  44050  diophren  44086  pell1qrval  44119  pell14qrval  44121  pell1234qrval  44123  pellfundval  44153  rmxypairf1o  44184  rmxyval  44188  mzpcong  44245  pw2f1ocnv  44310  dnnumch1  44317  dfac11  44330  hbtlem1  44390  hbtlem7  44392  elmnc  44403  dgraaval  44411  mpaaval  44418  itgoval  44428  flcidc  44433  mendval  44442  cytpval  44465  cantnfub  44584  cantnfresb  44587  tfsconcatrev  44611  elcnvlem  44862  comptiunov2i  44967  dftrcl3  44981  trclfvcom  44984  cnvtrclfv  44985  cotrcltrcl  44986  trclimalb2  44987  trclfvdecomr  44989  dfrtrcl3  44994  dfrtrcl4  44999  clsk1indlem0  45302  clsk1indlem2  45303  clsk1indlem3  45304  clsk1indlem4  45305  clsk1indlem1  45306  k0004val  45411  lhe4.4ex1a  45574  addrfv  45711  subrfv  45712  mulvfv  45713  monoord2xrv  46766  sumnnodd  46915  liminfgval  47045  ioodvbdlimc2lem  47217  itgsin0pilem1  47233  stoweidlem55  47338  wallispilem1  47348  wallispilem2  47349  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  dirkerval  47374  fourierdlem2  47392  fourierdlem3  47393  fourierdlem29  47419  fourierdlem62  47451  fourierdlem80  47469  fourierdlem103  47492  fourierdlem104  47493  fourierswlem  47513  fouriersw  47514  iundjiunlem  47742  carageniuncllem2  47805  0ome  47812  hoidmv1le  47877  hoidmvlelem3  47880  smflimsuplem7  48109  sqrtnnaa  48186  sqrtnzqaa  48187  sqrtnpoly  48216  iccpval  48770  fppr  49097  azval  49716  lazval  49725  bruval  49745  bigoval  49992  ackval0  50123  ackval41a  50137  oppcinito  50688  oppctermo  50689  dfinito4  50967  prstcval  51020  mndtcval  51048  setc1onsubc  51071  parswapval  51107  lmdfval2  51169  cmdfval2  51170  vsetrec  51202  onsetreclem1  51204  elpglem3  51212  pgindnf  51215  sinhval-named  51235  coshval-named  51236  tanhval  51247  secval  51268  cscval  51269  cotval  51270  aacllem  51367