MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpt Unicode version

Theorem fvmpt 5956
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
Assertion
Ref Expression
fvmpt
Distinct variable groups:   ,   ,   ,

Proof of Theorem fvmpt
StepHypRef Expression
1 fvmpt.3 . 2
2 fvmptg.1 . . 3
3 fvmptg.2 . . 3
42, 3fvmptg 5954 . 2
51, 4mpan2 671 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  e.cmpt 4510  `cfv 5593
This theorem is referenced by:  fvmptex  5966  ofval  6549  caofinvl  6567  fvresex  6773  1stval  6802  2ndval  6803  reldm  6851  curry1val  6893  curry2val  6897  fnwelem  6915  brtpos2  6980  onovuni  7032  tz7.44-1  7091  oasuc  7193  oesuclem  7194  omsuc  7195  onasuc  7197  onmsuc  7198  fvmptmap  7475  xpcomco  7627  unxpdomlem1  7744  unfilem2  7805  ordtypelem3  7966  ixpiunwdom  8038  inf3lema  8062  noinfep  8097  cantnfval  8108  cantnflem1d  8128  cantnflem1  8129  cantnfvalOLD  8138  cantnflem1dOLD  8151  cantnflem1OLD  8152  r1sucg  8208  r0weon  8411  infxpenc2lem1  8417  fseqenlem1  8426  fseqenlem2  8427  dfac8alem  8431  ac5num  8438  acni2  8448  dfac4  8524  dfac2a  8531  dfacacn  8542  dfac12lem1  8544  ackbij1lem7  8627  ackbij2lem2  8641  ackbij2lem3  8642  cfsmolem  8671  fin23lem28  8741  fin23lem39  8751  isf32lem6  8759  isf32lem7  8760  isf32lem8  8761  fin1a2lem3  8803  itunifval  8817  itunisuc  8820  axdc2lem  8849  axdc3lem2  8852  axcclem  8858  zorn2lem1  8897  negiso  10544  infmsup  10546  uzval  11112  flval  11931  ceilval  11967  ceilval2  11969  monoord2  12138  seqf1olem2  12147  seqf1o  12148  seqdistr  12158  serle  12162  seqof  12164  swrdfv  12651  revval  12734  revfv  12737  wwlktovf1  12895  wwlktovfo  12896  sgnval  12921  cjval  12935  reval  12939  imval  12940  sqrtval  13070  absval  13071  limsupval  13297  limsupgval  13299  climmpt  13394  climle  13462  rlimdiv  13468  isercolllem1  13487  isercoll2  13491  caurcvg2  13500  fsumser  13552  isumadd  13582  fsumcnv  13588  fsumrev  13594  fsumshft  13595  iserabs  13629  cvgcmp  13630  cvgcmpce  13632  incexclem  13648  isumless  13657  supcvg  13667  harmonic  13670  trireciplem  13673  trirecip  13674  expcnv  13675  explecnv  13676  geolim  13679  geolim2  13680  geo2lim  13684  geomulcvg  13685  geoisum  13686  geoisumr  13687  geoisum1  13688  geoisum1c  13689  cvgrat  13692  mertenslem2  13694  mertens  13695  prodfdiv  13705  fprodser  13756  fprodshft  13780  fprodrev  13781  fprodcnv  13787  iprodmul  13796  eftval  13812  efval  13815  efcvgfsum  13821  ege2le3  13825  eftlub  13844  eflegeo  13856  sinval  13857  cosval  13858  tanval  13863  eirrlem  13937  rpnnen2lem1  13948  rpnnen2lem2  13949  bitsfval  14073  bitsinv2  14093  bitsinv  14098  sadcf  14103  sadc0  14104  sadcp1  14105  smupf  14128  smup0  14129  smupp1  14130  qnumval  14270  qdenval  14271  phival  14297  crt  14308  phimullem  14309  eulerthlem2  14312  odzval  14318  iserodd  14359  pcmpt  14411  prmreclem1  14434  prmreclem2  14435  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  1arithlem1  14441  1arithlem2  14442  vdwapfval  14489  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  vdwlem9  14507  ramub1lem2  14545  ramcl  14547  strfvnd  14647  topnval  14832  prdsplusgfval  14871  prdsmulrfval  14873  isacs  15048  acsfn  15056  cidfval  15073  homffval  15086  comfffval  15093  oppcval  15108  monfval  15127  oppcmon  15133  sectffval  15145  invffval  15152  isoval  15159  idfuval  15245  homafval  15356  arwval  15370  idafval  15384  coafval  15391  yonedainv  15550  pltfval  15589  lubfval  15608  lubval  15614  glbfval  15621  glbval  15627  p0val  15671  p1val  15672  oduval  15760  ipoval  15784  plusffval  15877  grpidval  15887  issubm  15978  prdspjmhm  15998  grpinvfval  16088  grpinvval  16089  grpsubfval  16092  grplactfval  16136  grplactval  16137  mulgfval  16143  prdsinvlem  16178  pwsmulg  16184  issubg  16201  cycsubgcl  16227  isnsg  16230  conjghm  16297  conjnmz  16300  cntrval  16357  cntzfval  16358  cntzval  16359  oppgval  16382  symgval  16404  psgnfval  16525  psgnval  16532  odfval  16557  odval  16558  sylow1lem4  16621  pgpssslw  16634  sylow2blem3  16642  sylow3lem2  16648  lsmfval  16658  pj1fval  16712  efgval  16735  efgsval  16749  frgpval  16776  vrgpval  16785  mulgmhm  16836  mulgghm  16837  ablfaclem1  17136  mgpval  17144  srglmhm  17186  srgrmhm  17187  ringlghm  17250  ringrghm  17251  opprval  17273  dvdsrval  17294  isunit  17306  invrfval  17322  dvrfval  17333  isirred  17348  issubrg  17429  abvfval  17467  abvtrivd  17489  staffval  17496  stafval  17497  scaffval  17530  lmodvsghm  17571  lssset  17580  lspfval  17619  islbs  17722  sraval  17822  rlmval  17837  2idlval  17881  lpival  17893  rrgval  17935  fidomndrnglem  17955  aspval  17977  asclfval  17983  asclval  17984  psrmulval  18039  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvrval  18077  mvrval2  18078  mplmonmul  18126  evlslem3  18183  evlslem1  18184  evlsval  18188  evlssca  18191  evlsvar  18192  psr1val  18225  vr1val  18231  ply1val  18233  coe1fval  18244  coe1fv  18245  coe1tmmul2  18317  coe1tmmul  18318  coe1tmmul2fv  18319  coe1pwmulfv  18321  evls1val  18357  evl1fval  18364  evl1val  18365  expmhm  18485  expghm  18529  expghmOLD  18530  mulgghm2  18531  mulgrhm  18532  mulgghm2OLD  18534  mulgrhmOLD  18535  zrhval  18545  zrhmulg  18547  zlmval  18553  chrval  18562  znval  18572  znzrhval  18585  evpmss  18622  psgnevpmb  18623  ip0l  18671  ipffval  18683  ocvfval  18697  ocvval  18698  cssval  18713  thlval  18726  pjfval  18737  pjval  18741  isobs  18751  prdsinvgd2  18773  uvcresum  18824  frlmup1  18832  frlmup2  18833  islinds  18844  islindf5  18874  mamulid  18943  mamurid  18944  mdetleib  19089  mdetleib1  19093  mdetunilem9  19122  mdetuni0  19123  mdetmul  19125  cpmidpmatlem1  19371  ordtval  19690  cnpval  19737  ptpjpre1  20072  ptpjopn  20113  dfac14  20119  upxp  20124  uptx  20126  hauseqlcld  20147  txlm  20149  xkoptsub  20155  xkoinjcn  20188  kqval  20227  xpstopnlem1  20310  fmval  20444  flfval  20491  ptcmplem2  20553  ptcmplem3  20554  symgtgp  20600  qustgpopn  20618  ussval  20762  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  mopnval  20941  prdsxmslem2  21032  nmfval  21109  nmval  21110  nmoval  21222  metdsval  21351  divcn  21372  mulc1cncf  21409  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  cnheiborlem  21454  evth  21459  evth2  21460  lebnumlem3  21463  isphtpy  21481  isphtpc  21494  pcofval  21510  pcovalg  21512  pco1  21515  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevcl  21525  pcorevlem  21526  pcorev2  21528  pi1xfrcnv  21557  cphnm  21640  tchval  21661  tchnmval  21672  cfilfval  21703  iscmet  21723  iscmet3lem3  21729  rrxval  21819  ehlval  21837  ivth2  21867  ovolval  21885  ovollb2lem  21899  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovolicc1  21927  voliunlem1  21960  voliunlem2  21961  voliunlem3  21962  volsup  21966  ioorval  21983  uniioombllem3  21994  uniioombllem6  21997  volsup2  22014  volcn  22015  volivth  22016  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  vitali  22022  mbfmax  22056  mbfimaopnlem  22062  itg1val  22090  i1f1lem  22096  itg11  22098  itg1addlem4  22106  itg1mulc  22111  i1fres  22112  itg1climres  22121  mbfi1fseqlem2  22123  mbfi1fseqlem3  22124  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfi1flim  22130  mbfmullem2  22131  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  itg2cnlem1  22168  itg2cn  22170  limccnp2  22296  dvnff  22326  dvnp1  22328  cpnfval  22335  elcpn  22337  dvrec  22358  dvcnvlem  22377  dveflem  22380  dvef  22381  dvferm1  22386  dvferm2  22388  rolle  22391  dvlip  22394  dvlipcn  22395  dv11cn  22402  dvivthlem1  22409  dvivth  22411  lhop1lem  22414  ftc1lem1  22436  ftc1lem5  22441  ftc2  22445  itgsubstlem  22449  tdeglem3  22457  tdeglem4  22458  mdegval  22462  mdegvalOLD  22463  mdegmullem  22478  deg1fval  22480  deg1ldg  22492  deg1leb  22495  coe1mul3  22500  uc1pval  22540  mon1pval  22542  q1pval  22554  r1pval  22557  ply1remlem  22563  ig1pval  22573  plyval  22590  elply2  22593  plyeq0lem  22607  coeval  22620  dgrval  22625  coeid2  22636  coemullem  22647  coemul  22649  elqaalem1  22715  elqaalem2  22716  elqaalem3  22717  iaa  22721  aareccl  22722  aannenlem1  22724  geolim3  22735  aaliou3lem1  22738  aaliou3lem2  22739  aaliou3lem5  22743  aaliou3lem6  22744  aaliou3lem7  22745  aaliou3  22747  tayl0  22757  taylthlem1  22768  taylthlem2  22769  ulmshftlem  22784  ulmshft  22785  ulmuni  22787  ulmcau  22790  ulmdvlem1  22795  ulmdvlem3  22797  mtest  22799  mtestbdd  22800  mbfulm  22801  iblulm  22802  itgulm  22803  pserval  22805  pserval2  22806  radcnvlem1  22808  radcnvlem2  22809  dvradcnv  22816  pserulm  22817  pserdvlem2  22823  pserdv  22824  abelthlem1  22826  abelthlem3  22828  abelthlem4  22829  abelthlem5  22830  abelthlem6  22831  abelthlem7  22833  abelthlem8  22834  abelthlem9  22835  resinf1o  22923  efif1olem4  22932  eff1olem  22935  logcnlem5  23027  logtayllem  23040  logtayl  23041  logtaylsum  23042  logtayl2  23043  logccv  23044  asinval  23213  acosval  23214  atanval  23215  atantayl  23268  leibpilem2  23272  leibpi  23273  leibpisum  23274  log2cnv  23275  log2tlbnd  23276  areaval  23294  efrlim  23299  dfef2  23300  amgmlem  23319  emcllem2  23326  emcllem3  23327  emcllem4  23328  emcllem5  23329  emcllem6  23330  emcllem7  23331  ftalem7  23352  basellem2  23355  basellem3  23356  basellem4  23357  basellem5  23358  basellem6  23359  basellem8  23361  basellem9  23362  chtval  23384  vmaval  23387  chpval  23396  ppival  23401  muval  23406  prmorcht  23452  sqff1o  23456  dvdsflsumcom  23464  musum  23467  muinv  23469  sgmppw  23472  fsumvma  23488  pclogsum  23490  dchrfi  23530  bposlem5  23563  bposlem7  23565  bposlem8  23566  bposlem9  23567  lgsfval  23576  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  lgsqrlem2  23617  lgsqrlem4  23619  lgseisenlem2  23625  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasumiflem1  23686  dchrvmaeq0  23689  dchrisum0fval  23690  dchrisum0re  23698  mulog2sumlem1  23719  pntrval  23747  pntsval  23757  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntlem3  23794  abvcxp  23800  padicfval  23801  padicval  23802  padicabv  23815  ostth1  23818  ostth2  23822  ostth3  23823  iscgrg  23904  legval  23971  ishlg  23986  ishpg  24128  iscgra  24169  ttgval  24178  elee  24197  axsegconlem1  24220  axsegconlem9  24228  axsegconlem10  24229  axpasch  24244  axlowdimlem15  24259  axlowdim  24264  axeuclidlem  24265  axcontlem2  24268  eengv  24282  wlknwwlkninj  24711  wlknwwlknsur  24712  wlkiswwlkinj  24718  wlkiswwlksur  24719  wwlkextinj  24730  wwlkextsur  24731  clwwlkfv  24795  vdgrval  24896  rusgranumwlklem3  24951  numclwwlkfvc  25077  gidval  25215  grpoinvval  25227  bafval  25497  imsval  25591  dipfval  25612  sspval  25636  nmooval  25678  hmoval  25725  ipasslem8  25752  ipasslem9  25753  ipblnfi  25771  ubthlem2  25787  htthlem  25834  normval  26041  ocval  26198  occllem  26221  hsupval  26252  pjhfval  26314  pjhval  26315  chscllem2  26556  chscllem3  26557  hosval  26659  homval  26660  hodval  26661  hfsval  26662  hfmval  26663  brafval  26862  braval  26863  kbval  26873  eigvalval  26879  cnlnadjlem1  26986  nmopadjlei  27007  hmopidmchi  27070  strlem2  27170  hstrlem2  27178  cdj3lem2  27354  ofpreima  27507  inftmrel  27724  isinftm  27725  locfinreflem  27843  rmulccn  27910  xrmulc1cn  27912  xrge0iifcv  27916  xrge0iifiso  27917  xrge0iifhom  27919  xrge0iif1  27920  qqhval  27955  rrhval  27977  xrhval  27996  ddeval1  28206  ddeval0  28207  sxbrsigalem0  28242  sxbrsigalem3  28243  eulerpartlemgv  28312  rrvmbfm  28381  dstrvval  28409  coinflippv  28422  ballotlem2  28427  ballotlemfval  28428  ballotlemi  28439  ballotlemsval  28447  ballotlemrval  28456  ballotth  28476  plymulx  28505  signstfv  28520  signsvvfval  28535  zetacvg  28557  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulm2  28578  lgamcvglem  28582  igamval  28589  lgamcvg2  28597  gamcvg2lem  28601  derangval  28611  subfacval  28617  erdszelem3  28637  erdszelem9  28643  erdszelem10  28644  txpcon  28677  indispcon  28679  cvxpcon  28687  cvmlift2lem2  28749  cvmlift2lem3  28750  cvmlift2lem7  28754  cvmliftphtlem  28762  cvmlift3lem4  28767  snmlfval  28775  snmlval  28776  mvtval  28860  mvrsval  28865  mrsubffval  28867  mrsubcv  28870  mrsubrn  28873  elmrsubrn  28880  msubffval  28883  mvhfval  28893  mvhval  28894  mpstval  28895  msrfval  28897  mstaval  28904  mclsval  28923  mppsval  28932  sinccvglem  29038  circum  29040  divcnvshft  29117  divcnvlin  29118  iprodefisum  29124  iprodgam  29125  faclimlem1  29168  faclimlem2  29169  faclim  29171  iprodfac  29172  faclim2  29173  dfrdg2  29228  bpolylem  29810  findabrcl  29919  finixpnum  30038  mblfinlem2  30052  voliunnfl  30058  volsupnfl  30059  itg2addnclem  30066  itg2addnclem3  30068  ftc1cnnc  30089  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anc  30098  ftc2nc  30099  fvopabf4g  30211  sdclem2  30235  fdc  30238  lmclim2  30251  geomcau  30252  istotbnd  30265  isbnd  30276  prdsbnd2  30291  heiborlem6  30312  heiborlem7  30313  heiborlem8  30314  rrnval  30323  rrncmslem  30328  idlval  30410  pridlval  30430  maxidlval  30436  isnacs  30636  mzpclval  30657  mzpsubst  30681  mzprename  30682  mzpcompact2lem  30684  eldiophb  30690  diophrw  30692  eldioph2  30695  diophin  30706  diophun  30707  diophren  30747  pell1qrval  30782  pell14qrval  30784  pell1234qrval  30786  pellfundval  30816  rmxypairf1o  30847  rmxyval  30851  mzpcong  30910  pw2f1ocnv  30979  dnnumch1  30990  dfac11  31008  hbtlem1  31072  hbtlem7  31074  elmnc  31085  dgraaval  31093  mpaaval  31100  itgoval  31110  rgspnval  31117  flcidc  31123  mendval  31132  issdrg  31146  phisum  31159  mon1pid  31165  cytpval  31169  lhe4.4ex1a  31234  addrfv  31378  subrfv  31379  mulvfv  31380  sumnnodd  31636  ioodvbdlimc2lem  31731  itgsin0pilem1  31748  stoweidlem55  31837  wallispilem1  31847  wallispilem2  31848  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  dirkerval  31873  fourierdlem2  31891  fourierdlem3  31892  fourierdlem29  31918  fourierdlem62  31951  fourierdlem80  31969  fourierdlem103  31992  fourierdlem104  31993  fourierswlem  32013  fouriersw  32014  issubmgm  32477  sinhval-named  33130  coshval-named  33131  tanhval-named  33132  secval  33141  cscval  33142  cotval  33143  aacllem  33216  bj-inftyexpiinv  34611  bj-inftyexpidisj  34613  lshpset  34703  lsatset  34715  lcvfbr  34745  lflset  34784  lflnegcl  34800  lkrfval  34812  lshpkrlem1  34835  lshpkrlem2  34836  lshpkrlem3  34837  ldualset  34850  cmtfvalN  34935  cvrfval  34993  pats  35010  llnset  35229  lplnset  35253  lvolset  35296  lineset  35462  pointsetN  35465  psubspset  35468  pmapfval  35480  pmapval  35481  paddfval  35521  pclfvalN  35613  polfvalN  35628  polvalN  35629  psubclsetN  35660  watfvalN  35716  watvalN  35717  lhpset  35719  lautset  35806  pautsetN  35822  ldilfset  35832  ldilset  35833  ltrnfset  35841  ltrnset  35842  dilfsetN  35877  dilsetN  35878  trnfsetN  35880  trnsetN  35881  trlfset  35885  trlset  35886  trlval  35887  tgrpfset  36470  tgrpset  36471  tendofset  36484  tendoset  36485  tendo02  36513  tendoi  36520  erngfset  36525  erngset  36526  erngfset-rN  36533  erngset-rN  36534  cdlemksv  36570  dvafset  36730  dvaset  36731  dvaplusgv  36736  diaffval  36757  diafval  36758  diaval  36759  dvhfset  36807  dvhset  36808  cdlemm10N  36845  docaffvalN  36848  docafvalN  36849  djaffvalN  36860  djafvalN  36861  dibffval  36867  dibfval  36868  dibval  36869  dicffval  36901  dicfval  36902  dicval  36903  dihffval  36957  dihfval  36958  dihval  36959  dochffval  37076  dochfval  37077  djhffval  37123  djhfval  37124  dochfl1  37203  lpolsetN  37209  lcfrlem8  37276  lcdfval  37315  lcdval  37316  mapdffval  37353  mapdfval  37354  mapdhval  37451  hvmapffval  37485  hvmapfval  37486  hdmap1ffval  37523  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapffval  37615  hgmapfval  37616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601
  Copyright terms: Public domain W3C validator