Theorem fvmpt 6763

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ↦ cmpt 5115  ‘cfv 6339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-iota 6298  df-fun 6341  df-fv 6347

This theorem is referenced by:  fvmptex  6777  fvmptrabfv  6794  mptfvmpt  6987  ofval  7420  caofinvl  7439  fvresex  7670  1stval  7700  2ndval  7701  reldm  7752  curry1val  7810  curry2val  7814  fsplitfpar  7824  fnwelem  7835  brtpos2  7913  onovuni  7994  tz7.44-1  8057  oasuc  8164  oesuclem  8165  omsuc  8166  onasuc  8168  onmsuc  8169  fvmptmap  8468  xpcomco  8633  unxpdomlem1  8765  unfilem2  8821  ordtypelem3  9022  ixpiunwdom  9092  inf3lema  9125  noinfep  9161  cantnfval  9169  cantnflem1d  9189  cantnflem1  9190  r1sucg  9236  r0weon  9477  infxpenc2lem1  9484  fseqenlem1  9489  fseqenlem2  9490  dfac8alem  9494  ac5num  9501  acni2  9511  dfac4  9587  dfac2a  9594  dfacacn  9606  dfac12lem1  9608  ackbij1lem7  9691  ackbij2lem2  9705  ackbij2lem3  9706  cfsmolem  9735  fin23lem28  9805  fin23lem39  9815  isf32lem6  9823  isf32lem7  9824  isf32lem8  9825  fin1a2lem3  9867  itunifval  9881  itunisuc  9884  axdc2lem  9913  axdc3lem2  9916  axcclem  9922  zorn2lem1  9961  negiso  11662  infrenegsup  11665  uzval  12289  flval  13218  ceilval  13262  ceilval2  13264  monoord2  13456  seqf1olem2  13465  seqf1o  13466  seqdistr  13476  serle  13480  seqof  13482  swrdfv  14062  revval  14174  revfv  14177  wwlktovf1  14373  wwlktovfo  14374  sgnval  14500  cjval  14514  reval  14518  imval  14519  sqrtval  14649  absval  14650  limsupval  14884  limsupgval  14886  climmpt  14981  climle  15049  rlimdiv  15055  isercolllem1  15074  isercoll2  15078  caurcvg2  15087  fsumser  15140  isumadd  15175  fsumcnv  15181  fsumrev  15187  fsumshft  15188  iserabs  15223  cvgcmp  15224  cvgcmpce  15226  incexclem  15244  isumless  15253  divcnvshft  15263  supcvg  15264  harmonic  15267  trireciplem  15270  trirecip  15271  expcnv  15272  explecnv  15273  geolim  15279  geolim2  15280  geo2lim  15284  geomulcvg  15285  geoisum  15286  geoisumr  15287  geoisum1  15288  geoisum1c  15289  cvgrat  15292  mertenslem2  15294  mertens  15295  prodfdiv  15305  fprodser  15356  fprodshft  15383  fprodrev  15384  fprodcnv  15390  iprodmul  15410  bpolylem  15455  eftval  15483  efval  15486  efcvgfsum  15492  ege2le3  15496  eftlub  15515  eflegeo  15527  sinval  15528  cosval  15529  tanval  15534  eirrlem  15610  rpnnen2lem1  15620  rpnnen2lem2  15621  bitsfval  15827  bitsinv2  15847  bitsinv  15852  sadcf  15857  sadc0  15858  sadcp1  15859  smupf  15882  smup0  15883  smupp1  15884  qnumval  16137  qdenval  16138  phival  16164  crth  16175  phimullem  16176  eulerthlem2  16179  phisum  16187  odzval  16188  iserodd  16232  pcmpt  16288  prmreclem1  16312  prmreclem2  16313  prmreclem4  16315  prmreclem5  16316  prmreclem6  16317  1arithlem1  16319  1arithlem2  16320  vdwapfval  16367  vdwlem2  16378  vdwlem6  16382  vdwlem8  16384  vdwlem9  16385  ramub1lem2  16423  ramcl  16425  prmoval  16429  strfvnd  16565  topnval  16771  prdsplusgfval  16810  prdsmulrfval  16812  isacs  16985  acsfn  16993  homffval  17023  comfffval  17031  oppcval  17046  monfval  17066  oppcmon  17072  sectffval  17084  invffval  17092  isoval  17099  idfuval  17210  homafval  17360  arwval  17374  coafval  17395  yonedainv  17602  pltfval  17640  lubfval  17659  lubval  17665  glbfval  17672  glbval  17678  p0val  17722  p1val  17723  oduval  17811  ipoval  17835  plusffval  17929  grpidval  17942  issubm  18039  prdspjmhm  18064  efmnd  18106  smndex1igid  18140  grpinvfval  18214  grpinvval  18216  grpsubfval  18219  grpsubfvalALT  18220  grplactval  18273  prdsinvlem  18280  mulgfval  18298  mulgfvalALT  18299  pwsmulg  18344  issubg  18351  isnsg  18379  cycsubmel  18415  cycsubgcl  18421  conjghm  18461  conjnmz  18464  cntrval  18521  cntzfval  18522  cntzval  18523  oppgval  18547  psgnfval  18700  psgnval  18707  odfval  18732  odval  18734  sylow1lem4  18798  pgpssslw  18811  sylow2blem3  18819  sylow3lem2  18825  lsmfval  18835  pj1fval  18892  efgval  18915  efgsval  18929  frgpval  18956  vrgpval  18965  mulgmhm  19021  mulgghm  19022  ablfaclem1  19280  mgpval  19315  srglmhm  19358  srgrmhm  19359  ringlghm  19430  ringrghm  19431  opprval  19450  dvdsrval  19471  isunit  19483  invrfval  19499  dvrfval  19510  isirred  19525  issubrg  19608  issdrg  19647  abvfval  19662  abvtrivd  19684  staffval  19691  stafval  19692  scaffval  19725  lmodvsghm  19768  lssset  19778  lspfval  19818  islbs  19921  sraval  20021  rlmval  20036  2idlval  20079  lpival  20091  rrgval  20133  fidomndrnglem  20152  expmhm  20240  expghm  20270  mulgghm2  20271  mulgrhm  20272  zrhval  20282  zrhmulg  20284  zlmval  20290  chrval  20298  znval  20308  znzrhval  20319  evpmss  20356  psgnevpmb  20357  ip0l  20406  ipffval  20418  ocvfval  20436  ocvval  20437  cssval  20452  thlval  20465  pjfval  20476  pjval  20480  isobs  20490  prdsinvgd2  20512  uvcresum  20563  frlmup1  20568  frlmup2  20569  islinds  20579  islindf5  20609  aspval  20640  asclval  20647  psrmulval  20719  psrlidm  20736  psrridm  20737  mvrval  20754  mvrval2  20755  mplmonmul  20801  evlslem3  20848  evlslem1  20850  evlsval  20854  evlssca  20857  evlsvar  20858  psr1val  20915  vr1val  20921  ply1val  20923  coe1fval  20934  coe1fv  20935  coe1tmmul2  21005  coe1tmmul  21006  coe1tmmul2fv  21007  coe1pwmulfv  21009  evls1val  21044  evl1fval  21052  evl1val  21053  mamulid  21146  mamurid  21147  mdetleib  21292  mdetleib1  21296  mdetunilem9  21325  mdetuni0  21326  mdetmul  21328  cpmidpmatlem1  21575  ordtval  21894  cnpval  21941  ptpjpre1  22276  ptpjopn  22317  dfac14  22323  upxp  22328  uptx  22330  hauseqlcld  22351  txlm  22353  xkoptsub  22359  xkoinjcn  22392  kqval  22431  xpstopnlem1  22514  fmval  22648  flfval  22695  ptcmplem2  22758  ptcmplem3  22759  symgtgp  22811  qustgpopn  22825  ussval  22965  iscfilu  22994  ispsmet  23011  ismet  23030  isxmet  23031  mopnval  23145  prdsxmslem2  23236  nmfval  23295  nmval  23296  nmoval  23422  metdsval  23553  divcn  23574  mulc1cncf  23611  icopnfhmeo  23649  iccpnfhmeo  23651  xrhmeo  23652  cnheiborlem  23660  evth  23665  evth2  23666  lebnumlem3  23669  isphtpy  23687  isphtpc  23700  pcofval  23716  pcovalg  23718  pco1  23721  pcopt  23728  pcopt2  23729  pcoass  23730  pcorevcl  23731  pcorevlem  23732  pcorev2  23734  pi1xfrcnv  23763  cphnm  23899  tcphval  23923  tcphnmval  23934  cfilfval  23969  iscmet  23989  iscmet3lem3  23995  rrxval  24092  ehlval  24119  ivth2  24160  ovolval  24178  ovollb2lem  24193  ovolunlem1a  24201  ovolunlem1  24202  ovoliunlem1  24207  ovoliunlem2  24208  ovolicc1  24221  voliunlem1  24255  voliunlem2  24256  voliunlem3  24257  volsup  24261  ioorval  24279  uniioombllem3  24290  uniioombllem6  24293  volsup2  24310  volcn  24311  volivth  24312  vitalilem2  24314  vitalilem3  24315  vitalilem4  24316  vitali  24318  mbfmax  24354  mbfimaopnlem  24360  itg1val  24388  i1f1lem  24394  itg11  24396  itg1addlem4  24404  itg1mulc  24409  i1fres  24410  itg1climres  24419  mbfi1fseqlem2  24421  mbfi1fseqlem3  24422  mbfi1fseqlem6  24425  mbfi1flimlem  24427  mbfi1flim  24428  mbfmullem2  24429  itg2seq  24447  itg2uba  24448  itg2splitlem  24453  itg2monolem1  24455  itg2monolem2  24456  itg2monolem3  24457  itg2mono  24458  itg2i1fseqle  24459  itg2i1fseq  24460  itg2i1fseq2  24461  itg2addlem  24463  itg2cnlem1  24466  itg2cn  24468  limccnp2  24596  dvnff  24627  dvnp1  24629  cpnfval  24636  elcpn  24638  dvrec  24659  dvcnvlem  24680  dveflem  24683  dvef  24684  dvferm1  24689  dvferm2  24691  rolle  24694  dvlip  24697  dvlipcn  24698  dv11cn  24705  dvivthlem1  24712  dvivth  24714  lhop1lem  24717  ftc1lem1  24739  ftc1lem5  24744  ftc2  24748  itgsubstlem  24752  tdeglem3  24762  tdeglem3OLD  24763  tdeglem4  24764  tdeglem4OLD  24765  mdegval  24768  mdegmullem  24783  deg1fval  24785  deg1ldg  24797  deg1leb  24800  coe1mul3  24804  uc1pval  24844  mon1pval  24846  q1pval  24858  r1pval  24861  ply1remlem  24867  ig1pval  24877  plyval  24894  elply2  24897  plyeq0lem  24911  coeval  24924  dgrval  24929  coeid2  24940  coemullem  24951  coemul  24953  elqaalem1  25019  elqaalem2  25020  elqaalem3  25021  iaa  25025  aareccl  25026  aannenlem1  25028  geolim3  25039  aaliou3lem1  25042  aaliou3lem2  25043  aaliou3lem5  25047  aaliou3lem6  25048  aaliou3lem7  25049  aaliou3  25051  tayl0  25061  taylthlem1  25072  taylthlem2  25073  ulmshftlem  25088  ulmshft  25089  ulmuni  25091  ulmcau  25094  ulmdvlem1  25099  ulmdvlem3  25101  mtest  25103  mtestbdd  25104  mbfulm  25105  iblulm  25106  itgulm  25107  pserval  25109  pserval2  25110  radcnvlem1  25112  radcnvlem2  25113  dvradcnv  25120  pserulm  25121  pserdvlem2  25127  pserdv  25128  abelthlem1  25130  abelthlem3  25132  abelthlem4  25133  abelthlem5  25134  abelthlem6  25135  abelthlem7  25137  abelthlem8  25138  abelthlem9  25139  resinf1o  25232  efif1olem4  25241  eff1olem  25244  logcnlem5  25341  logtayllem  25354  logtayl  25355  logtaylsum  25356  logtayl2  25357  logccv  25358  asinval  25572  acosval  25573  atanval  25574  atantayl  25627  leibpilem2  25631  leibpi  25632  leibpisum  25633  log2cnv  25634  log2tlbnd  25635  areaval  25654  efrlim  25659  dfef2  25660  amgmlem  25679  emcllem2  25686  emcllem3  25687  emcllem4  25688  emcllem5  25689  emcllem6  25690  emcllem7  25691  zetacvg  25704  lgamgulmlem4  25721  lgamgulmlem5  25722  lgamgulm2  25725  lgamcvglem  25729  igamval  25736  lgamcvg2  25744  gamcvg2lem  25748  ftalem7  25768  basellem2  25771  basellem3  25772  basellem4  25773  basellem5  25774  basellem6  25775  basellem8  25777  basellem9  25778  chtval  25799  vmaval  25802  chpval  25811  ppival  25816  muval  25821  prmorcht  25867  sqff1o  25871  dvdsflsumcom  25877  musum  25880  muinv  25882  sgmppw  25885  fsumvma  25901  pclogsum  25903  dchrfi  25943  bposlem5  25976  bposlem7  25978  bposlem8  25979  bposlem9  25980  lgsfval  25990  lgsdir  26020  lgsdilem2  26021  lgsdi  26022  lgsne0  26023  lgsqrlem2  26035  lgsqrlem4  26037  lgseisenlem2  26064  dchrmusum2  26182  dchrvmasumlem1  26183  dchrvmasumiflem1  26189  dchrvmaeq0  26192  dchrisum0fval  26193  dchrisum0re  26201  mulog2sumlem1  26222  pntrval  26250  pntsval  26260  pntrlog2bndlem4  26268  pntrlog2bndlem5  26269  pntlem3  26297  abvcxp  26303  padicfval  26304  padicval  26305  padicabv  26318  ostth1  26321  ostth2  26325  ostth3  26326  iscgrg  26410  legval  26482  ishpg  26657  iscgra  26707  isinag  26736  isleag  26745  iseqlg  26765  ttgval  26773  elee  26792  axsegconlem1  26815  axsegconlem9  26823  axsegconlem10  26824  axpasch  26839  axlowdimlem15  26854  axlowdim  26859  axeuclidlem  26860  axcontlem2  26863  eengv  26877  vtxval  26897  iedgval  26898  edgval  26946  vtxdgval  27362  wwlksnextinj  27789  wwlksnextsurj  27790  clwwlkfv  27937  clwwlknonmpo  27978  fusgreg2wsplem  28222  fusgreghash2wsp  28227  numclwwlk1lem2fv  28245  gidval  28399  grpoinvval  28410  bafval  28491  imsval  28572  dipfval  28589  sspval  28610  nmooval  28650  hmoval  28697  ipasslem8  28724  ipasslem9  28725  ipblnfi  28742  ubthlem2  28758  htthlem  28804  normval  29011  ocval  29167  occllem  29190  hsupval  29221  pjhfval  29283  pjhval  29284  chscllem2  29525  chscllem3  29526  hosval  29627  homval  29628  hodval  29629  hfsval  29630  hfmval  29631  brafval  29830  braval  29831  kbval  29841  eigvalval  29847  cnlnadjlem1  29954  nmopadjlei  29975  hmopidmchi  30038  strlem2  30138  hstrlem2  30146  cdj3lem2  30322  ofpreima  30530  psgnfzto1stlem  30897  evpmval  30942  altgnsg  30946  inftmrel  30964  isinftm  30965  qusker  31074  qusvscpbl  31076  qusscaval  31077  mxidlval  31158  idlsrgval  31173  dimval  31211  dimvalfi  31212  smatfval  31270  lmatval  31288  locfinreflem  31315  rspecval  31339  rmulccn  31403  xrmulc1cn  31405  xrge0iifcv  31409  xrge0iifiso  31410  xrge0iifhom  31412  xrge0iif1  31413  qqhval  31447  rrhval  31469  xrhval  31491  ddeval1  31725  ddeval0  31726  sxbrsigalem0  31761  sxbrsigalem3  31762  eulerpartlemgv  31863  rrvmbfm  31932  dstrvval  31960  coinflippv  31973  ballotlem2  31978  ballotlemfval  31979  ballotlemi  31990  ballotlemsval  31998  ballotlemrval  32007  ballotth  32027  plymulx  32050  signstfv  32065  signsvvfval  32080  derangval  32649  subfacval  32655  erdszelem3  32675  erdszelem9  32681  erdszelem10  32682  txpconn  32714  indispconn  32716  cvxpconn  32724  cvmlift2lem2  32786  cvmlift2lem3  32787  cvmlift2lem7  32791  cvmliftphtlem  32799  cvmlift3lem4  32804  snmlfval  32812  snmlval  32813  gonafv  32832  mvtval  32982  mrsubffval  32989  mrsubcv  32992  mrsubrn  32995  elmrsubrn  33002  msubffval  33005  mvhval  33016  mpstval  33017  mstaval  33026  mclsval  33045  mppsval  33054  sinccvglem  33150  circum  33152  divcnvlin  33217  iprodefisum  33226  iprodgam  33227  faclimlem1  33228  faclimlem2  33229  faclim  33231  iprodfac  33232  faclim2  33233  dfrdg2  33291  nosupfv  33498  noinffv  33513  newval  33625  leftval  33629  rightval  33630  findabrcl  34218  dnival  34226  bj-evalval  34796  bj-inftyexpitaudisj  34926  bj-inftyexpiinv  34929  bj-inftyexpidisj  34931  curfv  35343  finixpnum  35348  poimirlem16  35379  poimir  35396  broucube  35397  mblfinlem2  35401  voliunnfl  35407  volsupnfl  35408  itg2addnclem  35414  itg2addnclem3  35416  ftc1cnnc  35435  ftc1anclem5  35440  ftc1anclem6  35441  ftc1anclem7  35442  ftc1anc  35444  ftc2nc  35445  fvopabf4g  35465  sdclem2  35486  fdc  35489  lmclim2  35502  geomcau  35503  istotbnd  35513  isbnd  35524  prdsbnd2  35539  heiborlem6  35560  heiborlem7  35561  heiborlem8  35562  rrnval  35571  rrncmslem  35576  idlval  35757  pridlval  35777  maxidlval  35783  lshpset  36580  lsatset  36592  lcvfbr  36622  lflset  36661  lflnegcl  36677  lshpkrlem1  36712  lshpkrlem2  36713  lshpkrlem3  36714  ldualset  36727  cmtfvalN  36812  cvrfval  36870  pats  36887  llnset  37107  lplnset  37131  lvolset  37174  lineset  37340  pointsetN  37343  psubspset  37346  pmapval  37359  paddfval  37399  pclfvalN  37491  polfvalN  37506  polvalN  37507  psubclsetN  37538  watvalN  37595  lhpset  37597  lautset  37684  pautsetN  37700  ldilset  37711  ltrnset  37720  dilsetN  37755  trnsetN  37758  trlset  37763  trlval  37764  tgrpset  38347  tendoset  38361  tendo02  38389  erngset  38402  erngset-rN  38410  cdlemksv  38446  dvaset  38607  dvaplusgv  38612  diafval  38633  diaval  38634  dvhset  38683  cdlemm10N  38720  docafvalN  38724  djafvalN  38736  dibfval  38743  dibval  38744  dicfval  38777  dicval  38778  dihval  38834  dochfval  38952  djhfval  38999  dochfl1  39078  lpolsetN  39084  lcdval  39191  mapdhval  39326  hvmapfval  39361  hdmap1fval  39398  pwspjmhmmgpd  39802  pwsexpg  39803  mhphf  39818  prjspval  39967  isnacs  40046  mzpclval  40067  mzpsubst  40090  mzprename  40091  mzpcompact2lem  40093  eldiophb  40099  diophrw  40101  eldioph2  40104  diophin  40114  diophun  40115  diophren  40155  pell1qrval  40188  pell14qrval  40190  pell1234qrval  40192  pellfundval  40222  rmxypairf1o  40253  rmxyval  40257  mzpcong  40314  pw2f1ocnv  40379  dnnumch1  40389  dfac11  40407  hbtlem1  40468  hbtlem7  40470  elmnc  40481  dgraaval  40489  mpaaval  40496  itgoval  40506  rgspnval  40513  flcidc  40519  mendval  40528  mon1pid  40550  cytpval  40554  elcnvlem  40702  comptiunov2i  40808  dftrcl3  40822  trclfvcom  40825  cnvtrclfv  40826  cotrcltrcl  40827  trclimalb2  40828  trclfvdecomr  40830  dfrtrcl3  40835  dfrtrcl4  40840  clsk1indlem0  41145  clsk1indlem2  41146  clsk1indlem3  41147  clsk1indlem4  41148  clsk1indlem1  41149  k0004val  41254  lhe4.4ex1a  41434  addrfv  41574  subrfv  41575  mulvfv  41576  monoord2xrv  42517  sumnnodd  42666  liminfgval  42798  ioodvbdlimc2lem  42970  itgsin0pilem1  42986  stoweidlem55  43091  wallispilem1  43101  wallispilem2  43102  wallispilem4  43104  wallispi2lem1  43107  wallispi2lem2  43108  dirkerval  43127  fourierdlem2  43145  fourierdlem3  43146  fourierdlem29  43172  fourierdlem62  43204  fourierdlem80  43222  fourierdlem103  43245  fourierdlem104  43246  fourierswlem  43266  fouriersw  43267  iundjiunlem  43492  carageniuncllem2  43555  0ome  43562  hoidmv1le  43627  hoidmvlelem3  43630  smflimsuplem7  43851  iccpval  44328  fppr  44639  issubmgm  44804  bigoval  45356  ackval0  45487  ackval41a  45501  eenglngeehlnm  45546  vsetrec  45696  onsetreclem1  45698  elpglem3  45706  sinhval-named  45726  coshval-named  45727  tanhval-named  45728  secval  45737  cscval  45738  cotval  45739  aacllem  45793