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

Theorem fvmpt 5618
Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
Hypotheses
Ref Expression
fvmptg.1  |-  ( x  =  A  ->  B  =  C )
fvmptg.2  |-  F  =  ( x  e.  D  |->  B )
fvmpt.3  |-  C  e. 
_V
Assertion
Ref Expression
fvmpt  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Distinct variable groups:    x, A    x, C    x, D
Allowed substitution hints:    B( x)    F( x)

Proof of Theorem fvmpt
StepHypRef Expression
1 fvmpt.3 . 2  |-  C  e. 
_V
2 fvmptg.1 . . 3  |-  ( x  =  A  ->  B  =  C )
3 fvmptg.2 . . 3  |-  F  =  ( x  e.  D  |->  B )
42, 3fvmptg 5616 . 2  |-  ( ( A  e.  D  /\  C  e.  _V )  ->  ( F `  A
)  =  C )
51, 4mpan2 652 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   _Vcvv 2801    e. cmpt 4093   ` cfv 5271
This theorem is referenced by:  fvmptex  5626  fvresex  5778  ofval  6103  caofinvl  6120  1stval  6140  2ndval  6141  reldm  6187  curry1val  6227  curry2val  6231  fnwelem  6246  brtpos2  6256  onovuni  6375  tz7.44-1  6435  oasuc  6539  oesuclem  6540  omsuc  6541  onasuc  6543  onmsuc  6544  fvmptmap  6820  xpcomco  6968  unxpdomlem1  7083  unfilem2  7138  ordtypelem3  7251  ixpiunwdom  7321  inf3lema  7341  noinfep  7376  cantnfval  7385  cantnflem1d  7406  cantnflem1  7407  r1sucg  7457  r0weon  7656  infxpenc2lem1  7662  fseqenlem1  7667  fseqenlem2  7668  dfac8alem  7672  ac5num  7679  acni2  7689  dfac4  7765  dfac2a  7772  dfacacn  7783  dfac12lem1  7785  ackbij1lem7  7868  ackbij2lem2  7882  ackbij2lem3  7883  cfsmolem  7912  fin23lem28  7982  fin23lem39  7992  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  fin1a2lem3  8044  itunifval  8058  itunisuc  8061  axdc2lem  8090  axdc3lem2  8093  axcclem  8099  zorn2lem1  8139  negiso  9746  infmsup  9748  uzval  10248  flval  10942  monoord2  11093  seqf1olem2  11102  seqf1o  11103  seqdistr  11113  serle  11117  seqof  11119  swrdfv  11473  revval  11494  revfv  11497  cjval  11603  reval  11607  imval  11608  sqrval  11738  absval  11739  limsupval  11964  limsupgval  11966  climmpt  12061  climle  12129  rlimdiv  12135  isercolllem1  12154  isercoll2  12158  caurcvg2  12166  fsumser  12219  isumadd  12246  fsumcnv  12252  fsumrev  12257  fsumshft  12258  iserabs  12289  cvgcmp  12290  cvgcmpce  12292  incexclem  12311  isumless  12320  supcvg  12330  harmonic  12333  trireciplem  12336  trirecip  12337  expcnv  12338  explecnv  12339  geolim  12342  geolim2  12343  geo2lim  12347  geomulcvg  12348  geoisum  12349  geoisumr  12350  geoisum1  12351  geoisum1c  12352  cvgrat  12355  mertenslem2  12357  mertens  12358  eftval  12374  efval  12377  efcvgfsum  12383  ege2le3  12387  eftlub  12405  eflegeo  12417  sinval  12418  cosval  12419  tanval  12424  eirrlem  12498  rpnnen2lem1  12509  rpnnen2lem2  12510  bitsfval  12630  bitsinv2  12650  bitsinv  12655  sadcf  12660  sadc0  12661  sadcp1  12662  smupf  12685  smup0  12686  smupp1  12687  qnumval  12824  qdenval  12825  phival  12851  crt  12862  phimullem  12863  eulerthlem2  12866  odzval  12872  iserodd  12904  pcmpt  12956  prmreclem1  12979  prmreclem2  12980  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  1arithlem1  12986  1arithlem2  12987  vdwapfval  13034  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  ramub1lem2  13090  ramcl  13092  strfvnd  13179  topnval  13355  prdsplusgfval  13389  prdsmulrfval  13391  isacs  13569  acsfn  13577  cidfval  13594  homffval  13610  comfffval  13617  oppcval  13632  monfval  13651  oppcmon  13657  sectffval  13669  invffval  13676  isoval  13683  idfuval  13766  homafval  13877  arwval  13891  idafval  13905  coafval  13912  yonedainv  14071  pltfval  14109  lubfval  14128  lubval  14129  glbfval  14133  glbval  14134  joinfval  14137  meetfval  14144  p0val  14163  p1val  14164  oduval  14250  ipoval  14273  plusffval  14395  grpidval  14400  issubm  14441  prdspjmhm  14459  grpinvfval  14536  grpinvval  14537  grpsubfval  14540  grplactfval  14578  grplactval  14579  mulgfval  14584  prdsinvlem  14619  pwsmulg  14625  issubg  14637  cycsubgcl  14659  isnsg  14662  conjghm  14729  conjnmz  14732  symgval  14787  cntrval  14811  cntzfval  14812  cntzval  14813  oppgval  14836  odfval  14864  odval  14865  sylow1lem4  14928  pgpssslw  14941  sylow2blem3  14949  sylow3lem2  14955  lsmfval  14965  pj1fval  15019  efgval  15042  efgsval  15056  frgpval  15083  vrgpval  15092  mulgmhm  15143  mulgghm  15144  ablfaclem1  15336  mgpval  15344  rnglghm  15404  rngrghm  15405  opprval  15422  dvdsrval  15443  isunit  15455  invrfval  15471  dvrfval  15482  isirred  15497  issubrg  15561  abvfval  15599  abvtrivd  15621  staffval  15628  stafval  15629  scaffval  15661  lmodvsghm  15702  lssset  15707  lspfval  15746  islbs  15845  sraval  15945  rlmval  15961  2idlval  16001  lpival  16013  rrgval  16044  fidomndrnglem  16063  aspval  16084  asclfval  16090  asclval  16091  psrmulval  16147  psrlidm  16164  psrridm  16165  mvrval  16182  mvrval2  16183  mplmonmul  16224  psr1val  16281  vr1val  16287  ply1val  16289  coe1fval  16302  coe1fv  16303  coe1tmmul2  16368  coe1tmmul  16369  coe1tmmul2fv  16370  coe1pwmulfv  16372  expmhm  16465  expghm  16466  mulgghm2  16475  mulgrhm  16476  zrhval  16478  zrhmulg  16480  zlmval  16486  chrval  16495  znval  16505  znzrhval  16516  ip0l  16556  ipffval  16568  ocvfval  16582  ocvval  16583  cssval  16598  thlval  16611  pjfval  16622  pjval  16626  isobs  16636  ordtval  16935  cnpval  16982  ptpjpre1  17282  ptpjopn  17322  dfac14  17328  upxp  17333  uptx  17335  hauseqlcld  17356  txlm  17358  xkoptsub  17364  xkoinjcn  17397  kqval  17433  xpstopnlem1  17516  fmval  17654  flfval  17701  ptcmplem2  17763  ptcmplem3  17764  symgtgp  17800  divstgpopn  17818  ismet  17904  isxmet  17905  mopnval  18000  prdsxmslem2  18091  nmfval  18127  nmval  18128  nmoval  18240  metdsval  18367  divcn  18388  mulc1cncf  18425  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  cnheiborlem  18468  evth  18473  evth2  18474  lebnumlem3  18477  isphtpy  18495  isphtpc  18508  pcofval  18524  pcovalg  18526  pco1  18529  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevcl  18539  pcorevlem  18540  pcorev2  18542  pi1xfrcnv  18571  cphnm  18645  tchval  18666  tchnmval  18676  cfilfval  18706  iscmet  18726  iscmet3lem3  18732  ivth2  18831  ovolval  18849  ovollb2lem  18863  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovolicc1  18891  voliunlem1  18923  voliunlem2  18924  voliunlem3  18925  volsup  18929  ioorval  18945  uniioombllem3  18956  uniioombllem6  18959  volsup2  18976  volcn  18977  volivth  18978  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  vitali  18984  mbfmax  19020  mbfimaopnlem  19026  itg1val  19054  i1f1lem  19060  itg11  19062  itg1addlem4  19070  itg1mulc  19075  i1fres  19076  itg1climres  19085  mbfi1fseqlem2  19087  mbfi1fseqlem3  19088  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfi1flim  19094  mbfmullem2  19095  itg2seq  19113  itg2uba  19114  itg2splitlem  19119  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  itg2cnlem1  19132  itg2cn  19134  limccnp2  19258  dvnff  19288  dvnp1  19290  cpnfval  19297  elcpn  19299  dvrec  19320  dvcnvlem  19339  dveflem  19342  dvef  19343  dvferm1  19348  dvferm2  19350  rolle  19353  dvlip  19356  dvlipcn  19357  dv11cn  19364  dvivthlem1  19371  dvivth  19373  lhop1lem  19376  ftc1lem1  19398  ftc1lem5  19403  ftc2  19407  itgsubstlem  19411  evlslem3  19414  evlslem1  19415  evlsval  19419  evlssca  19422  evlsvar  19423  evl1fval  19426  evl1val  19427  tdeglem3  19461  tdeglem4  19462  mdegval  19465  mdegmullem  19480  deg1fval  19482  deg1ldg  19494  deg1leb  19497  coe1mul3  19501  uc1pval  19541  mon1pval  19543  q1pval  19555  r1pval  19558  ply1remlem  19564  ig1pval  19574  plyval  19591  elply2  19594  plyeq0lem  19608  coeval  19621  dgrval  19626  coeid2  19637  coemullem  19647  coemul  19649  elqaalem1  19715  elqaalem2  19716  elqaalem3  19717  iaa  19721  aareccl  19722  aannenlem1  19724  geolim3  19735  aaliou3lem1  19738  aaliou3lem2  19739  aaliou3lem5  19743  aaliou3lem6  19744  aaliou3lem7  19745  aaliou3  19747  tayl0  19757  taylthlem1  19768  taylthlem2  19769  ulmshftlem  19784  ulmshft  19785  ulmcau  19788  ulmdvlem1  19793  ulmdvlem3  19795  mtest  19797  mbfulm  19798  iblulm  19799  itgulm  19800  pserval  19802  pserval2  19803  radcnvlem1  19805  radcnvlem2  19806  dvradcnv  19813  pserulm  19814  pserdvlem2  19820  pserdv  19821  abelthlem1  19823  abelthlem3  19825  abelthlem4  19826  abelthlem5  19827  abelthlem6  19828  abelthlem7  19830  abelthlem8  19831  abelthlem9  19832  resinf1o  19914  efgh  19919  efif1olem4  19923  eff1olem  19926  logcnlem5  20009  logtayllem  20022  logtayl  20023  logtaylsum  20024  logtayl2  20025  logccv  20026  asinval  20194  acosval  20195  atanval  20196  atantayl  20249  leibpilem2  20253  leibpi  20254  leibpisum  20255  log2cnv  20256  log2tlbnd  20257  areaval  20275  efrlim  20280  dfef2  20281  amgmlem  20300  emcllem2  20306  emcllem3  20307  emcllem4  20308  emcllem5  20309  emcllem6  20310  emcllem7  20311  ftalem7  20332  basellem2  20335  basellem3  20336  basellem4  20337  basellem5  20338  basellem6  20339  basellem8  20341  basellem9  20342  chtval  20364  vmaval  20367  chpval  20376  ppival  20381  muval  20386  prmorcht  20432  sqff1o  20436  dvdsflsumcom  20444  musum  20447  muinv  20449  sgmppw  20452  fsumvma  20468  pclogsum  20470  dchrfi  20510  bposlem5  20543  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgsfval  20556  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  lgsqrlem2  20597  lgsqrlem4  20599  lgseisenlem2  20605  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasumiflem1  20666  dchrvmaeq0  20669  dchrisum0fval  20670  dchrisum0re  20678  mulog2sumlem1  20699  pntrval  20727  pntsval  20737  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntlem3  20774  abvcxp  20780  padicfval  20781  padicval  20782  padicabv  20795  ostth1  20798  ostth2  20802  ostth3  20803  gidval  20896  grpoinvval  20908  bafval  21176  imsval  21270  dipfval  21291  sspval  21315  nmooval  21357  hmoval  21404  ipasslem8  21431  ipasslem9  21432  ipblnfi  21450  ubthlem2  21466  htthlem  21513  normval  21719  ocval  21875  occllem  21898  hsupval  21929  pjhfval  21991  pjhval  21992  chscllem2  22233  chscllem3  22234  hosval  22336  homval  22337  hodval  22338  hfsval  22339  hfmval  22340  brafval  22539  braval  22540  kbval  22550  eigvalval  22556  cnlnadjlem1  22663  nmopadjlei  22684  hmopidmchi  22747  strlem2  22847  hstrlem2  22855  cdj3lem2  23031  ballotlem2  23063  ballotlemfval  23064  ballotlemi  23075  ballotlemsval  23083  ballotlemrval  23092  ballotth  23112  rmulccn  23316  xrmulc1cn  23318  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhom  23334  xrge0iif1  23335  dya2iocrrnval  23597  rrvmbfm  23660  dstrvval  23686  coinflippv  23699  zetacvg  23704  dmgmseqn0  23711  derangval  23713  subfacval  23719  erdszelem3  23739  erdszelem9  23745  erdszelem10  23746  txpcon  23778  indispcon  23780  cvxpcon  23788  cvmlift2lem2  23850  cvmlift2lem3  23851  cvmlift2lem7  23855  cvmliftphtlem  23863  cvmlift3lem4  23868  vdgrval  23905  snmlfval  23928  snmlval  23929  sinccvglem  24020  circum  24022  faclimlem3  24119  faclimlem5  24121  faclimlem7  24123  faclim  24126  dfrdg2  24223  elee  24594  axsegconlem1  24617  axsegconlem9  24625  axsegconlem10  24626  axpasch  24641  axlowdimlem15  24656  axlowdim  24661  axeuclidlem  24662  axcontlem2  24665  bpolylem  24855  findabrcl  24965  itg2addnclem  25003  itg2addnc  25005  ftc1cnnc  25025  valpr  25261  prjmapcp2  25273  valvalcurfn  25309  gepsup  25353  seinf  25354  fprodser  25423  fincmpzer  25453  rltrooo  25518  idlvalNEW  25548  cntrset  25705  isaddrv  25749  issubcv  25773  ishoma  25890  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  cinvlem2  25932  issubcat  25948  vtarsu  25989  trclval  25997  domcatfun  26028  codcatfun  26037  isrocatset  26060  iscatset  26081  isconcl1b  26200  fvopabf4g  26489  sdclem2  26555  fdc  26558  lmclim2  26577  geomcau  26578  istotbnd  26596  isbnd  26607  prdsbnd2  26622  heiborlem6  26643  heiborlem7  26644  heiborlem8  26645  rrnval  26654  rrncmslem  26659  idlval  26741  pridlval  26761  maxidlval  26767  isnacs  26882  mzpclval  26906  mzpsubst  26929  mzprename  26930  mzpcompact2lem  26932  eldiophb  26939  diophrw  26941  eldioph2  26944  diophin  26955  diophun  26956  diophren  26999  pell1qrval  27034  pell14qrval  27036  pell1234qrval  27038  pellfundval  27068  rmxypairf1o  27099  rmxyval  27103  mzpcong  27162  pw2f1ocnv  27233  dnnumch1  27244  dfac11  27263  prdsinvgd2  27311  uvcresum  27345  frlmup1  27353  frlmup2  27354  islinds  27382  islindf5  27412  hbtlem1  27430  hbtlem7  27432  elmnc  27444  dgraaval  27452  mpaaval  27459  itgoval  27469  rgspnval  27476  flcidc  27482  psgnfval  27526  psgnval  27533  mamulid  27561  mamurid  27562  mdetleib  27591  mendval  27594  issdrg  27608  phisum  27621  mon1pid  27627  cytpval  27631  lhe4.4ex1a  27649  addrfv  27777  subrfv  27778  mulvfv  27779  itgsin0pilem1  27847  stoweidlem55  27907  wallispilem1  27917  wallispilem2  27918  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  sinhval-named  28460  coshval-named  28461  tanhval-named  28462  secval  28471  cscval  28472  cotval  28473  sgnval  28499  ceilingval  28509  lshpset  29790  lsatset  29802  lcvfbr  29832  lflset  29871  lflnegcl  29887  lkrfval  29899  lshpkrlem1  29922  lshpkrlem2  29923  lshpkrlem3  29924  ldualset  29937  cmtfvalN  30022  cvrfval  30080  pats  30097  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  pointsetN  30552  psubspset  30555  pmapfval  30567  pmapval  30568  paddfval  30608  pclfvalN  30700  polfvalN  30715  polvalN  30716  psubclsetN  30747  watfvalN  30803  watvalN  30804  lhpset  30806  lautset  30893  pautsetN  30909  ldilfset  30919  ldilset  30920  ltrnfset  30928  ltrnset  30929  dilfsetN  30963  dilsetN  30964  trnfsetN  30966  trnsetN  30967  trlfset  30971  trlset  30972  trlval  30973  tgrpfset  31555  tgrpset  31556  tendofset  31569  tendoset  31570  tendo02  31598  tendoi  31605  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  cdlemksv  31655  dvafset  31815  dvaset  31816  dvaplusgv  31821  diaffval  31842  diafval  31843  diaval  31844  dvhfset  31892  dvhset  31893  cdlemm10N  31930  docaffvalN  31933  docafvalN  31934  djaffvalN  31945  djafvalN  31946  dibffval  31952  dibfval  31953  dibval  31954  dicffval  31986  dicfval  31987  dicval  31988  dihffval  32042  dihfval  32043  dihval  32044  dochffval  32161  dochfval  32162  djhffval  32208  djhfval  32209  dochfl1  32288  lpolsetN  32294  lcfrlem8  32361  lcdfval  32400  lcdval  32401  mapdffval  32438  mapdfval  32439  mapdhval  32536  hvmapffval  32570  hvmapfval  32571  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279
  Copyright terms: Public domain W3C validator