Theorem fvmpt 6857

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvmptex  6871  fvmptrabfv  6888  mptfvmpt  7086  ofval  7522  caofinvl  7541  fvresex  7776  1stval  7806  2ndval  7807  reldm  7858  curry1val  7916  curry2val  7920  fsplitfpar  7930  fnwelem  7943  brtpos2  8019  onovuni  8144  tz7.44-1  8208  oasuc  8316  oesuclem  8317  omsuc  8318  onasuc  8320  onmsuc  8321  fvmptmap  8627  xpcomco  8802  unxpdomlem1  8956  unfilem2  9009  ordtypelem3  9209  ixpiunwdom  9279  inf3lema  9312  noinfep  9348  cantnfval  9356  cantnflem1d  9376  cantnflem1  9377  r1sucg  9458  r0weon  9699  infxpenc2lem1  9706  fseqenlem1  9711  fseqenlem2  9712  dfac8alem  9716  ac5num  9723  acni2  9733  dfac4  9809  dfac2a  9816  dfacacn  9828  dfac12lem1  9830  ackbij1lem7  9913  ackbij2lem2  9927  ackbij2lem3  9928  cfsmolem  9957  fin23lem28  10027  fin23lem39  10037  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  fin1a2lem3  10089  itunifval  10103  itunisuc  10106  axdc2lem  10135  axdc3lem2  10138  axcclem  10144  zorn2lem1  10183  negiso  11885  infrenegsup  11888  uzval  12513  flval  13442  ceilval  13486  ceilval2  13488  monoord2  13682  seqf1olem2  13691  seqf1o  13692  seqdistr  13702  serle  13706  seqof  13708  swrdfv  14289  revval  14401  revfv  14404  wwlktovf1  14600  wwlktovfo  14601  sgnval  14727  cjval  14741  reval  14745  imval  14746  sqrtval  14876  absval  14877  limsupval  15111  limsupgval  15113  climmpt  15208  climle  15277  rlimdiv  15285  isercolllem1  15304  isercoll2  15308  caurcvg2  15317  fsumser  15370  isumadd  15407  fsumcnv  15413  fsumrev  15419  fsumshft  15420  iserabs  15455  cvgcmp  15456  cvgcmpce  15458  incexclem  15476  isumless  15485  divcnvshft  15495  supcvg  15496  harmonic  15499  trireciplem  15502  trirecip  15503  expcnv  15504  explecnv  15505  geolim  15510  geolim2  15511  geo2lim  15515  geomulcvg  15516  geoisum  15517  geoisumr  15518  geoisum1  15519  geoisum1c  15520  cvgrat  15523  mertenslem2  15525  mertens  15526  prodfdiv  15536  fprodser  15587  fprodshft  15614  fprodrev  15615  fprodcnv  15621  iprodmul  15641  bpolylem  15686  eftval  15714  efval  15717  efcvgfsum  15723  ege2le3  15727  eftlub  15746  eflegeo  15758  sinval  15759  cosval  15760  tanval  15765  eirrlem  15841  rpnnen2lem1  15851  rpnnen2lem2  15852  bitsfval  16058  bitsinv2  16078  bitsinv  16083  sadcf  16088  sadc0  16089  sadcp1  16090  smupf  16113  smup0  16114  smupp1  16115  qnumval  16369  qdenval  16370  phival  16396  crth  16407  phimullem  16408  eulerthlem2  16411  phisum  16419  odzval  16420  iserodd  16464  pcmpt  16521  prmreclem1  16545  prmreclem2  16546  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  1arithlem1  16552  1arithlem2  16553  vdwapfval  16600  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  vdwlem9  16618  ramub1lem2  16656  ramcl  16658  prmoval  16662  strfvnd  16814  topnval  17062  prdsplusgfval  17102  prdsmulrfval  17104  isacs  17277  acsfn  17285  homffval  17316  comfffval  17324  oppcval  17339  monfval  17361  oppcmon  17367  sectffval  17379  invffval  17387  isoval  17394  idfuval  17507  homafval  17660  arwval  17674  coafval  17695  yonedainv  17915  oduval  17922  pltfval  17964  lubfval  17983  lubval  17989  glbfval  17996  glbval  18002  p0val  18060  p1val  18061  ipoval  18163  plusffval  18247  grpidval  18260  issubm  18357  prdspjmhm  18382  efmnd  18424  smndex1igid  18458  grpinvfval  18533  grpinvval  18535  grpsubfval  18538  grpsubfvalALT  18539  grplactval  18592  prdsinvlem  18599  mulgfval  18617  mulgfvalALT  18618  pwsmulg  18663  issubg  18670  isnsg  18698  cycsubmel  18734  cycsubgcl  18740  conjghm  18780  conjnmz  18783  cntrval  18840  cntzfval  18841  cntzval  18842  oppgval  18866  psgnfval  19023  psgnval  19030  odfval  19055  odval  19057  sylow1lem4  19121  pgpssslw  19134  sylow2blem3  19142  sylow3lem2  19148  lsmfval  19158  pj1fval  19215  efgval  19238  efgsval  19252  frgpval  19279  vrgpval  19288  mulgmhm  19344  mulgghm  19345  ablfaclem1  19603  mgpval  19638  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  opprval  19778  dvdsrval  19802  isunit  19814  invrfval  19830  dvrfval  19841  isirred  19856  issubrg  19939  issdrg  19978  abvfval  19993  abvtrivd  20015  staffval  20022  stafval  20023  scaffval  20056  lmodvsghm  20099  lssset  20110  lspfval  20150  islbs  20253  sraval  20353  rlmval  20374  2idlval  20417  lpival  20429  rrgval  20471  fidomndrnglem  20491  expmhm  20579  expghm  20609  mulgghm2  20610  mulgrhm  20611  zrhval  20621  zrhmulg  20623  zlmval  20629  chrval  20641  znval  20651  znzrhval  20666  evpmss  20703  psgnevpmb  20704  ip0l  20753  ipffval  20765  ocvfval  20783  ocvval  20784  cssval  20799  thlval  20812  pjfval  20823  pjval  20827  isobs  20837  prdsinvgd2  20859  uvcresum  20910  frlmup1  20915  frlmup2  20916  islinds  20926  islindf5  20956  aspval  20987  asclval  20994  psrmulval  21065  psrlidm  21082  psrridm  21083  mvrval  21100  mvrval2  21101  mplmonmul  21147  evlslem3  21200  evlslem1  21202  evlsval  21206  evlssca  21209  evlsvar  21210  psr1val  21267  vr1val  21273  ply1val  21275  coe1fval  21286  coe1fv  21287  coe1tmmul2  21357  coe1tmmul  21358  coe1tmmul2fv  21359  coe1pwmulfv  21361  evls1val  21396  evl1fval  21404  evl1val  21405  mamulid  21498  mamurid  21499  mdetleib  21644  mdetleib1  21648  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  cpmidpmatlem1  21927  ordtval  22248  cnpval  22295  ptpjpre1  22630  ptpjopn  22671  dfac14  22677  upxp  22682  uptx  22684  hauseqlcld  22705  txlm  22707  xkoptsub  22713  xkoinjcn  22746  kqval  22785  xpstopnlem1  22868  fmval  23002  flfval  23049  ptcmplem2  23112  ptcmplem3  23113  symgtgp  23165  qustgpopn  23179  ussval  23319  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  mopnval  23499  prdsxmslem2  23591  nmfval  23650  nmval  23651  nmoval  23785  metdsval  23916  divcn  23937  mulc1cncf  23974  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  cnheiborlem  24023  evth  24028  evth2  24029  lebnumlem3  24032  isphtpy  24050  isphtpc  24063  pcofval  24079  pcovalg  24081  pco1  24084  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevcl  24094  pcorevlem  24095  pcorev2  24097  pi1xfrcnv  24126  cphnm  24262  tcphval  24287  tcphnmval  24298  cfilfval  24333  iscmet  24353  iscmet3lem3  24359  rrxval  24456  ehlval  24483  ivth2  24524  ovolval  24542  ovollb2lem  24557  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovolicc1  24585  voliunlem1  24619  voliunlem2  24620  voliunlem3  24621  volsup  24625  ioorval  24643  uniioombllem3  24654  uniioombllem6  24657  volsup2  24674  volcn  24675  volivth  24676  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  vitali  24682  mbfmax  24718  mbfimaopnlem  24724  itg1val  24752  i1f1lem  24758  itg11  24760  itg1addlem4  24768  itg1addlem4OLD  24769  itg1mulc  24774  i1fres  24775  itg1climres  24784  mbfi1fseqlem2  24786  mbfi1fseqlem3  24787  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfi1flim  24793  mbfmullem2  24794  itg2seq  24812  itg2uba  24813  itg2splitlem  24818  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  itg2cnlem1  24831  itg2cn  24833  limccnp2  24961  dvnff  24992  dvnp1  24994  cpnfval  25001  elcpn  25003  dvrec  25024  dvcnvlem  25045  dveflem  25048  dvef  25049  dvferm1  25054  dvferm2  25056  rolle  25059  dvlip  25062  dvlipcn  25063  dv11cn  25070  dvivthlem1  25077  dvivth  25079  lhop1lem  25082  ftc1lem1  25104  ftc1lem5  25109  ftc2  25113  itgsubstlem  25117  tdeglem3  25127  tdeglem3OLD  25128  tdeglem4  25129  tdeglem4OLD  25130  mdegval  25133  mdegmullem  25148  deg1fval  25150  deg1ldg  25162  deg1leb  25165  coe1mul3  25169  uc1pval  25209  mon1pval  25211  q1pval  25223  r1pval  25226  ply1remlem  25232  ig1pval  25242  plyval  25259  elply2  25262  plyeq0lem  25276  coeval  25289  dgrval  25294  coeid2  25305  coemullem  25316  coemul  25318  elqaalem1  25384  elqaalem2  25385  elqaalem3  25386  iaa  25390  aareccl  25391  aannenlem1  25393  geolim3  25404  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  aaliou3  25416  tayl0  25426  taylthlem1  25437  taylthlem2  25438  ulmshftlem  25453  ulmshft  25454  ulmuni  25456  ulmcau  25459  ulmdvlem1  25464  ulmdvlem3  25466  mtest  25468  mtestbdd  25469  mbfulm  25470  iblulm  25471  itgulm  25472  pserval  25474  pserval2  25475  radcnvlem1  25477  radcnvlem2  25478  dvradcnv  25485  pserulm  25486  pserdvlem2  25492  pserdv  25493  abelthlem1  25495  abelthlem3  25497  abelthlem4  25498  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  resinf1o  25597  efif1olem4  25606  eff1olem  25609  logcnlem5  25706  logtayllem  25719  logtayl  25720  logtaylsum  25721  logtayl2  25722  logccv  25723  asinval  25937  acosval  25938  atanval  25939  atantayl  25992  leibpilem2  25996  leibpi  25997  leibpisum  25998  log2cnv  25999  log2tlbnd  26000  areaval  26019  efrlim  26024  dfef2  26025  amgmlem  26044  emcllem2  26051  emcllem3  26052  emcllem4  26053  emcllem5  26054  emcllem6  26055  emcllem7  26056  zetacvg  26069  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulm2  26090  lgamcvglem  26094  igamval  26101  lgamcvg2  26109  gamcvg2lem  26113  ftalem7  26133  basellem2  26136  basellem3  26137  basellem4  26138  basellem5  26139  basellem6  26140  basellem8  26142  basellem9  26143  chtval  26164  vmaval  26167  chpval  26176  ppival  26181  muval  26186  prmorcht  26232  sqff1o  26236  dvdsflsumcom  26242  musum  26245  muinv  26247  sgmppw  26250  fsumvma  26266  pclogsum  26268  dchrfi  26308  bposlem5  26341  bposlem7  26343  bposlem8  26344  bposlem9  26345  lgsfval  26355  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgsqrlem2  26400  lgsqrlem4  26402  lgseisenlem2  26429  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0fval  26558  dchrisum0re  26566  mulog2sumlem1  26587  pntrval  26615  pntsval  26625  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntlem3  26662  abvcxp  26668  padicfval  26669  padicval  26670  padicabv  26683  ostth1  26686  ostth2  26690  ostth3  26691  iscgrg  26777  legval  26849  ishpg  27024  iscgra  27074  isinag  27103  isleag  27112  iseqlg  27132  ttgval  27140  elee  27165  axsegconlem1  27188  axsegconlem9  27196  axsegconlem10  27197  axpasch  27212  axlowdimlem15  27227  axlowdim  27232  axeuclidlem  27233  axcontlem2  27236  eengv  27250  vtxval  27273  iedgval  27274  edgval  27322  vtxdgval  27738  wwlksnextinj  28165  wwlksnextsurj  28166  clwwlkfv  28313  clwwlknonmpo  28354  fusgreg2wsplem  28598  fusgreghash2wsp  28603  numclwwlk1lem2fv  28621  gidval  28775  grpoinvval  28786  bafval  28867  imsval  28948  dipfval  28965  sspval  28986  nmooval  29026  hmoval  29073  ipasslem8  29100  ipasslem9  29101  ipblnfi  29118  ubthlem2  29134  htthlem  29180  normval  29387  ocval  29543  occllem  29566  hsupval  29597  pjhfval  29659  pjhval  29660  chscllem2  29901  chscllem3  29902  hosval  30003  homval  30004  hodval  30005  hfsval  30006  hfmval  30007  brafval  30206  braval  30207  kbval  30217  eigvalval  30223  cnlnadjlem1  30330  nmopadjlei  30351  hmopidmchi  30414  strlem2  30514  hstrlem2  30522  cdj3lem2  30698  ofpreima  30904  psgnfzto1stlem  31269  evpmval  31314  altgnsg  31318  inftmrel  31336  isinftm  31337  qusker  31451  qusvscpbl  31453  qusscaval  31454  mxidlval  31535  idlsrgval  31550  dimval  31588  dimvalfi  31589  smatfval  31647  lmatval  31665  locfinreflem  31692  rspecval  31716  rmulccn  31780  xrmulc1cn  31782  xrge0iifcv  31786  xrge0iifiso  31787  xrge0iifhom  31789  xrge0iif1  31790  qqhval  31824  rrhval  31846  xrhval  31868  ddeval1  32102  ddeval0  32103  sxbrsigalem0  32138  sxbrsigalem3  32139  eulerpartlemgv  32240  rrvmbfm  32309  dstrvval  32337  coinflippv  32350  ballotlem2  32355  ballotlemfval  32356  ballotlemi  32367  ballotlemsval  32375  ballotlemrval  32384  ballotth  32404  plymulx  32427  signstfv  32442  signsvvfval  32457  derangval  33029  subfacval  33035  erdszelem3  33055  erdszelem9  33061  erdszelem10  33062  txpconn  33094  indispconn  33096  cvxpconn  33104  cvmlift2lem2  33166  cvmlift2lem3  33167  cvmlift2lem7  33171  cvmliftphtlem  33179  cvmlift3lem4  33184  snmlfval  33192  snmlval  33193  gonafv  33212  mvtval  33362  mrsubffval  33369  mrsubcv  33372  mrsubrn  33375  elmrsubrn  33382  msubffval  33385  mvhval  33396  mpstval  33397  mstaval  33406  mclsval  33425  mppsval  33434  sinccvglem  33530  circum  33532  divcnvlin  33604  iprodefisum  33613  iprodgam  33614  faclimlem1  33615  faclimlem2  33616  faclim  33618  iprodfac  33619  faclim2  33620  dfrdg2  33677  ssttrcl  33701  ttrcltr  33702  ttrclselem2  33712  nosupfv  33836  noinffv  33851  newval  33966  leftval  33974  rightval  33975  findabrcl  34570  dnival  34578  bj-evalval  35173  bj-inftyexpitaudisj  35303  bj-inftyexpiinv  35306  bj-inftyexpidisj  35308  curfv  35684  finixpnum  35689  poimirlem16  35720  poimir  35737  broucube  35738  mblfinlem2  35742  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  itg2addnclem3  35757  ftc1cnnc  35776  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anc  35785  ftc2nc  35786  fvopabf4g  35806  sdclem2  35827  fdc  35830  lmclim2  35843  geomcau  35844  istotbnd  35854  isbnd  35865  prdsbnd2  35880  heiborlem6  35901  heiborlem7  35902  heiborlem8  35903  rrnval  35912  rrncmslem  35917  idlval  36098  pridlval  36118  maxidlval  36124  lshpset  36919  lsatset  36931  lcvfbr  36961  lflset  37000  lflnegcl  37016  lshpkrlem1  37051  lshpkrlem2  37052  lshpkrlem3  37053  ldualset  37066  cmtfvalN  37151  cvrfval  37209  pats  37226  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  pointsetN  37682  psubspset  37685  pmapval  37698  paddfval  37738  pclfvalN  37830  polfvalN  37845  polvalN  37846  psubclsetN  37877  watvalN  37934  lhpset  37936  lautset  38023  pautsetN  38039  ldilset  38050  ltrnset  38059  dilsetN  38094  trnsetN  38097  trlset  38102  trlval  38103  tgrpset  38686  tendoset  38700  tendo02  38728  erngset  38741  erngset-rN  38749  cdlemksv  38785  dvaset  38946  dvaplusgv  38951  diafval  38972  diaval  38973  dvhset  39022  cdlemm10N  39059  docafvalN  39063  djafvalN  39075  dibfval  39082  dibval  39083  dicfval  39116  dicval  39117  dihval  39173  dochfval  39291  djhfval  39338  dochfl1  39417  lpolsetN  39423  lcdval  39530  mapdhval  39665  hvmapfval  39700  hdmap1fval  39737  pwspjmhmmgpd  40192  pwsexpg  40193  mhphf  40208  prjspval  40363  isnacs  40442  mzpclval  40463  mzpsubst  40486  mzprename  40487  mzpcompact2lem  40489  eldiophb  40495  diophrw  40497  eldioph2  40500  diophin  40510  diophun  40511  diophren  40551  pell1qrval  40584  pell14qrval  40586  pell1234qrval  40588  pellfundval  40618  rmxypairf1o  40649  rmxyval  40653  mzpcong  40710  pw2f1ocnv  40775  dnnumch1  40785  dfac11  40803  hbtlem1  40864  hbtlem7  40866  elmnc  40877  dgraaval  40885  mpaaval  40892  itgoval  40902  rgspnval  40909  flcidc  40915  mendval  40924  mon1pid  40946  cytpval  40950  elcnvlem  41098  comptiunov2i  41203  dftrcl3  41217  trclfvcom  41220  cnvtrclfv  41221  cotrcltrcl  41222  trclimalb2  41223  trclfvdecomr  41225  dfrtrcl3  41230  dfrtrcl4  41235  clsk1indlem0  41540  clsk1indlem2  41541  clsk1indlem3  41542  clsk1indlem4  41543  clsk1indlem1  41544  k0004val  41649  lhe4.4ex1a  41836  addrfv  41976  subrfv  41977  mulvfv  41978  monoord2xrv  42914  sumnnodd  43061  liminfgval  43193  ioodvbdlimc2lem  43365  itgsin0pilem1  43381  stoweidlem55  43486  wallispilem1  43496  wallispilem2  43497  wallispilem4  43499  wallispi2lem1  43502  wallispi2lem2  43503  dirkerval  43522  fourierdlem2  43540  fourierdlem3  43541  fourierdlem29  43567  fourierdlem62  43599  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  fourierswlem  43661  fouriersw  43662  iundjiunlem  43887  carageniuncllem2  43950  0ome  43957  hoidmv1le  44022  hoidmvlelem3  44025  smflimsuplem7  44246  iccpval  44755  fppr  45066  issubmgm  45231  bigoval  45783  ackval0  45914  ackval41a  45928  eenglngeehlnm  45973  prstcval  46233  mndtcval  46252  vsetrec  46294  onsetreclem1  46296  elpglem3  46304  sinhval-named  46324  coshval-named  46325  tanhval-named  46326  secval  46335  cscval  46336  cotval  46337  aacllem  46391