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

Theorem fvmpt 5602
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 5600 . 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 1623    e. wcel 1684   _Vcvv 2788    e. cmpt 4077   ` cfv 5255
This theorem is referenced by:  fvmptex  5610  fvresex  5762  ofval  6087  caofinvl  6104  1stval  6124  2ndval  6125  reldm  6171  curry1val  6211  curry2val  6215  fnwelem  6230  brtpos2  6240  onovuni  6359  tz7.44-1  6419  oasuc  6523  oesuclem  6524  omsuc  6525  onasuc  6527  onmsuc  6528  fvmptmap  6804  xpcomco  6952  unxpdomlem1  7067  unfilem2  7122  ordtypelem3  7235  ixpiunwdom  7305  inf3lema  7325  noinfep  7360  cantnfval  7369  cantnflem1d  7390  cantnflem1  7391  r1sucg  7441  r0weon  7640  infxpenc2lem1  7646  fseqenlem1  7651  fseqenlem2  7652  dfac8alem  7656  ac5num  7663  acni2  7673  dfac4  7749  dfac2a  7756  dfacacn  7767  dfac12lem1  7769  ackbij1lem7  7852  ackbij2lem2  7866  ackbij2lem3  7867  cfsmolem  7896  fin23lem28  7966  fin23lem39  7976  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  fin1a2lem3  8028  itunifval  8042  itunisuc  8045  axdc2lem  8074  axdc3lem2  8077  axcclem  8083  zorn2lem1  8123  negiso  9730  infmsup  9732  uzval  10232  flval  10926  monoord2  11077  seqf1olem2  11086  seqf1o  11087  seqdistr  11097  serle  11101  seqof  11103  swrdfv  11457  revval  11478  revfv  11481  cjval  11587  reval  11591  imval  11592  sqrval  11722  absval  11723  limsupval  11948  limsupgval  11950  climmpt  12045  climle  12113  rlimdiv  12119  isercolllem1  12138  isercoll2  12142  caurcvg2  12150  fsumser  12203  isumadd  12230  fsumcnv  12236  fsumrev  12241  fsumshft  12242  iserabs  12273  cvgcmp  12274  cvgcmpce  12276  incexclem  12295  isumless  12304  supcvg  12314  harmonic  12317  trireciplem  12320  trirecip  12321  expcnv  12322  explecnv  12323  geolim  12326  geolim2  12327  geo2lim  12331  geomulcvg  12332  geoisum  12333  geoisumr  12334  geoisum1  12335  geoisum1c  12336  cvgrat  12339  mertenslem2  12341  mertens  12342  eftval  12358  efval  12361  efcvgfsum  12367  ege2le3  12371  eftlub  12389  eflegeo  12401  sinval  12402  cosval  12403  tanval  12408  eirrlem  12482  rpnnen2lem1  12493  rpnnen2lem2  12494  bitsfval  12614  bitsinv2  12634  bitsinv  12639  sadcf  12644  sadc0  12645  sadcp1  12646  smupf  12669  smup0  12670  smupp1  12671  qnumval  12808  qdenval  12809  phival  12835  crt  12846  phimullem  12847  eulerthlem2  12850  odzval  12856  iserodd  12888  pcmpt  12940  prmreclem1  12963  prmreclem2  12964  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  1arithlem1  12970  1arithlem2  12971  vdwapfval  13018  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  ramub1lem2  13074  ramcl  13076  strfvnd  13163  topnval  13339  prdsplusgfval  13373  prdsmulrfval  13375  isacs  13553  acsfn  13561  cidfval  13578  homffval  13594  comfffval  13601  oppcval  13616  monfval  13635  oppcmon  13641  sectffval  13653  invffval  13660  isoval  13667  idfuval  13750  homafval  13861  arwval  13875  idafval  13889  coafval  13896  yonedainv  14055  pltfval  14093  lubfval  14112  lubval  14113  glbfval  14117  glbval  14118  joinfval  14121  meetfval  14128  p0val  14147  p1val  14148  oduval  14234  ipoval  14257  plusffval  14379  grpidval  14384  issubm  14425  prdspjmhm  14443  grpinvfval  14520  grpinvval  14521  grpsubfval  14524  grplactfval  14562  grplactval  14563  mulgfval  14568  prdsinvlem  14603  pwsmulg  14609  issubg  14621  cycsubgcl  14643  isnsg  14646  conjghm  14713  conjnmz  14716  symgval  14771  cntrval  14795  cntzfval  14796  cntzval  14797  oppgval  14820  odfval  14848  odval  14849  sylow1lem4  14912  pgpssslw  14925  sylow2blem3  14933  sylow3lem2  14939  lsmfval  14949  pj1fval  15003  efgval  15026  efgsval  15040  frgpval  15067  vrgpval  15076  mulgmhm  15127  mulgghm  15128  ablfaclem1  15320  mgpval  15328  rnglghm  15388  rngrghm  15389  opprval  15406  dvdsrval  15427  isunit  15439  invrfval  15455  dvrfval  15466  isirred  15481  issubrg  15545  abvfval  15583  abvtrivd  15605  staffval  15612  stafval  15613  scaffval  15645  lmodvsghm  15686  lssset  15691  lspfval  15730  islbs  15829  sraval  15929  rlmval  15945  2idlval  15985  lpival  15997  rrgval  16028  fidomndrnglem  16047  aspval  16068  asclfval  16074  asclval  16075  psrmulval  16131  psrlidm  16148  psrridm  16149  mvrval  16166  mvrval2  16167  mplmonmul  16208  psr1val  16265  vr1val  16271  ply1val  16273  coe1fval  16286  coe1fv  16287  coe1tmmul2  16352  coe1tmmul  16353  coe1tmmul2fv  16354  coe1pwmulfv  16356  expmhm  16449  expghm  16450  mulgghm2  16459  mulgrhm  16460  zrhval  16462  zrhmulg  16464  zlmval  16470  chrval  16479  znval  16489  znzrhval  16500  ip0l  16540  ipffval  16552  ocvfval  16566  ocvval  16567  cssval  16582  thlval  16595  pjfval  16606  pjval  16610  isobs  16620  ordtval  16919  cnpval  16966  ptpjpre1  17266  ptpjopn  17306  dfac14  17312  upxp  17317  uptx  17319  hauseqlcld  17340  txlm  17342  xkoptsub  17348  xkoinjcn  17381  kqval  17417  xpstopnlem1  17500  fmval  17638  flfval  17685  ptcmplem2  17747  ptcmplem3  17748  symgtgp  17784  divstgpopn  17802  ismet  17888  isxmet  17889  mopnval  17984  prdsxmslem2  18075  nmfval  18111  nmval  18112  nmoval  18224  metdsval  18351  divcn  18372  mulc1cncf  18409  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  cnheiborlem  18452  evth  18457  evth2  18458  lebnumlem3  18461  isphtpy  18479  isphtpc  18492  pcofval  18508  pcovalg  18510  pco1  18513  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevcl  18523  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  cphnm  18629  tchval  18650  tchnmval  18660  cfilfval  18690  iscmet  18710  iscmet3lem3  18716  ivth2  18815  ovolval  18833  ovollb2lem  18847  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovolicc1  18875  voliunlem1  18907  voliunlem2  18908  voliunlem3  18909  volsup  18913  ioorval  18929  uniioombllem3  18940  uniioombllem6  18943  volsup2  18960  volcn  18961  volivth  18962  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  vitali  18968  mbfmax  19004  mbfimaopnlem  19010  itg1val  19038  i1f1lem  19044  itg11  19046  itg1addlem4  19054  itg1mulc  19059  i1fres  19060  itg1climres  19069  mbfi1fseqlem2  19071  mbfi1fseqlem3  19072  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfi1flim  19078  mbfmullem2  19079  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  itg2cnlem1  19116  itg2cn  19118  limccnp2  19242  dvnff  19272  dvnp1  19274  cpnfval  19281  elcpn  19283  dvrec  19304  dvcnvlem  19323  dveflem  19326  dvef  19327  dvferm1  19332  dvferm2  19334  rolle  19337  dvlip  19340  dvlipcn  19341  dv11cn  19348  dvivthlem1  19355  dvivth  19357  lhop1lem  19360  ftc1lem1  19382  ftc1lem5  19387  ftc2  19391  itgsubstlem  19395  evlslem3  19398  evlslem1  19399  evlsval  19403  evlssca  19406  evlsvar  19407  evl1fval  19410  evl1val  19411  tdeglem3  19445  tdeglem4  19446  mdegval  19449  mdegmullem  19464  deg1fval  19466  deg1ldg  19478  deg1leb  19481  coe1mul3  19485  uc1pval  19525  mon1pval  19527  q1pval  19539  r1pval  19542  ply1remlem  19548  ig1pval  19558  plyval  19575  elply2  19578  plyeq0lem  19592  coeval  19605  dgrval  19610  coeid2  19621  coemullem  19631  coemul  19633  elqaalem1  19699  elqaalem2  19700  elqaalem3  19701  iaa  19705  aareccl  19706  aannenlem1  19708  geolim3  19719  aaliou3lem1  19722  aaliou3lem2  19723  aaliou3lem5  19727  aaliou3lem6  19728  aaliou3lem7  19729  aaliou3  19731  tayl0  19741  taylthlem1  19752  taylthlem2  19753  ulmshftlem  19768  ulmshft  19769  ulmcau  19772  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  mbfulm  19782  iblulm  19783  itgulm  19784  pserval  19786  pserval2  19787  radcnvlem1  19789  radcnvlem2  19790  dvradcnv  19797  pserulm  19798  pserdvlem2  19804  pserdv  19805  abelthlem1  19807  abelthlem3  19809  abelthlem4  19810  abelthlem5  19811  abelthlem6  19812  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  resinf1o  19898  efgh  19903  efif1olem4  19907  eff1olem  19910  logcnlem5  19993  logtayllem  20006  logtayl  20007  logtaylsum  20008  logtayl2  20009  logccv  20010  asinval  20178  acosval  20179  atanval  20180  atantayl  20233  leibpilem2  20237  leibpi  20238  leibpisum  20239  log2cnv  20240  log2tlbnd  20241  areaval  20259  efrlim  20264  dfef2  20265  amgmlem  20284  emcllem2  20290  emcllem3  20291  emcllem4  20292  emcllem5  20293  emcllem6  20294  emcllem7  20295  ftalem7  20316  basellem2  20319  basellem3  20320  basellem4  20321  basellem5  20322  basellem6  20323  basellem8  20325  basellem9  20326  chtval  20348  vmaval  20351  chpval  20360  ppival  20365  muval  20370  prmorcht  20416  sqff1o  20420  dvdsflsumcom  20428  musum  20431  muinv  20433  sgmppw  20436  fsumvma  20452  pclogsum  20454  dchrfi  20494  bposlem5  20527  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgsfval  20540  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  lgsqrlem2  20581  lgsqrlem4  20583  lgseisenlem2  20589  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasumiflem1  20650  dchrvmaeq0  20653  dchrisum0fval  20654  dchrisum0re  20662  mulog2sumlem1  20683  pntrval  20711  pntsval  20721  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntlem3  20758  abvcxp  20764  padicfval  20765  padicval  20766  padicabv  20779  ostth1  20782  ostth2  20786  ostth3  20787  gidval  20880  grpoinvval  20892  bafval  21160  imsval  21254  dipfval  21275  sspval  21299  nmooval  21341  hmoval  21388  ipasslem8  21415  ipasslem9  21416  ipblnfi  21434  ubthlem2  21450  htthlem  21497  normval  21703  ocval  21859  occllem  21882  hsupval  21913  pjhfval  21975  pjhval  21976  chscllem2  22217  chscllem3  22218  hosval  22320  homval  22321  hodval  22322  hfsval  22323  hfmval  22324  brafval  22523  braval  22524  kbval  22534  eigvalval  22540  cnlnadjlem1  22647  nmopadjlei  22668  hmopidmchi  22731  strlem2  22831  hstrlem2  22839  cdj3lem2  23015  ballotlem2  23047  ballotlemfval  23048  ballotlemi  23059  ballotlemsval  23067  ballotlemrval  23076  ballotth  23096  rmulccn  23301  xrmulc1cn  23303  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhom  23319  xrge0iif1  23320  dya2iocrrnval  23582  rrvmbfm  23645  dstrvval  23671  coinflippv  23684  zetacvg  23689  dmgmseqn0  23696  derangval  23698  subfacval  23704  erdszelem3  23724  erdszelem9  23730  erdszelem10  23731  txpcon  23763  indispcon  23765  cvxpcon  23773  cvmlift2lem2  23835  cvmlift2lem3  23836  cvmlift2lem7  23840  cvmliftphtlem  23848  cvmlift3lem4  23853  vdgrval  23890  snmlfval  23913  snmlval  23914  sinccvglem  24005  circum  24007  dfrdg2  24152  elee  24522  axsegconlem1  24545  axsegconlem9  24553  axsegconlem10  24554  axpasch  24569  axlowdimlem15  24584  axlowdim  24589  axeuclidlem  24590  axcontlem2  24593  bpolylem  24783  findabrcl  24893  valpr  25158  prjmapcp2  25170  valvalcurfn  25206  gepsup  25250  seinf  25251  fprodser  25320  fincmpzer  25350  rltrooo  25415  idlvalNEW  25445  cntrset  25602  isaddrv  25646  issubcv  25670  ishoma  25787  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  cinvlem2  25829  issubcat  25845  vtarsu  25886  trclval  25894  domcatfun  25925  codcatfun  25934  isrocatset  25957  iscatset  25978  isconcl1b  26097  fvopabf4g  26386  sdclem2  26452  fdc  26455  lmclim2  26474  geomcau  26475  istotbnd  26493  isbnd  26504  prdsbnd2  26519  heiborlem6  26540  heiborlem7  26541  heiborlem8  26542  rrnval  26551  rrncmslem  26556  idlval  26638  pridlval  26658  maxidlval  26664  isnacs  26779  mzpclval  26803  mzpsubst  26826  mzprename  26827  mzpcompact2lem  26829  eldiophb  26836  diophrw  26838  eldioph2  26841  diophin  26852  diophun  26853  diophren  26896  pell1qrval  26931  pell14qrval  26933  pell1234qrval  26935  pellfundval  26965  rmxypairf1o  26996  rmxyval  27000  mzpcong  27059  pw2f1ocnv  27130  dnnumch1  27141  dfac11  27160  prdsinvgd2  27208  uvcresum  27242  frlmup1  27250  frlmup2  27251  islinds  27279  islindf5  27309  hbtlem1  27327  hbtlem7  27329  elmnc  27341  dgraaval  27349  mpaaval  27356  itgoval  27366  rgspnval  27373  flcidc  27379  psgnfval  27423  psgnval  27430  mamulid  27458  mamurid  27459  mdetleib  27488  mendval  27491  issdrg  27505  phisum  27518  mon1pid  27524  cytpval  27528  lhe4.4ex1a  27546  addrfv  27674  subrfv  27675  mulvfv  27676  itgsin0pilem1  27744  stoweidlem55  27804  wallispilem1  27814  wallispilem2  27815  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  sinhval-named  28206  coshval-named  28207  tanhval-named  28208  secval  28217  cscval  28218  cotval  28219  sgnval  28245  ceilingval  28255  lshpset  29168  lsatset  29180  lcvfbr  29210  lflset  29249  lflnegcl  29265  lkrfval  29277  lshpkrlem1  29300  lshpkrlem2  29301  lshpkrlem3  29302  ldualset  29315  cmtfvalN  29400  cvrfval  29458  pats  29475  llnset  29694  lplnset  29718  lvolset  29761  lineset  29927  pointsetN  29930  psubspset  29933  pmapfval  29945  pmapval  29946  paddfval  29986  pclfvalN  30078  polfvalN  30093  polvalN  30094  psubclsetN  30125  watfvalN  30181  watvalN  30182  lhpset  30184  lautset  30271  pautsetN  30287  ldilfset  30297  ldilset  30298  ltrnfset  30306  ltrnset  30307  dilfsetN  30341  dilsetN  30342  trnfsetN  30344  trnsetN  30345  trlfset  30349  trlset  30350  trlval  30351  tgrpfset  30933  tgrpset  30934  tendofset  30947  tendoset  30948  tendo02  30976  tendoi  30983  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  cdlemksv  31033  dvafset  31193  dvaset  31194  dvaplusgv  31199  diaffval  31220  diafval  31221  diaval  31222  dvhfset  31270  dvhset  31271  cdlemm10N  31308  docaffvalN  31311  docafvalN  31312  djaffvalN  31323  djafvalN  31324  dibffval  31330  dibfval  31331  dibval  31332  dicffval  31364  dicfval  31365  dicval  31366  dihffval  31420  dihfval  31421  dihval  31422  dochffval  31539  dochfval  31540  djhffval  31586  djhfval  31587  dochfl1  31666  lpolsetN  31672  lcfrlem8  31739  lcdfval  31778  lcdval  31779  mapdffval  31816  mapdfval  31817  mapdhval  31914  hvmapffval  31948  hvmapfval  31949  hdmap1ffval  31986  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapffval  32078  hgmapfval  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263
  Copyright terms: Public domain W3C validator