Theorem fvmpt 6884

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ↦ cmpt 5158  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fvmptex  6898  fvmptrabfv  6915  mptfvmpt  7113  fvmptopab  7338  ofval  7553  caofinvl  7572  fvresex  7811  1stval  7842  2ndval  7843  reldm  7894  curry1val  7954  curry2val  7958  fsplitfpar  7968  fnwelem  7981  brtpos2  8057  onovuni  8182  tz7.44-1  8246  oasuc  8363  oesuclem  8364  omsuc  8365  onasuc  8367  onmsuc  8368  fvmptmap  8678  xpcomco  8858  unxpdomlem1  9036  unfilem2  9088  ordtypelem3  9288  ixpiunwdom  9358  inf3lema  9391  noinfep  9427  cantnfval  9435  cantnflem1d  9455  cantnflem1  9456  ssttrcl  9482  ttrcltr  9483  ttrclselem2  9493  r1sucg  9536  r0weon  9777  infxpenc2lem1  9784  fseqenlem1  9789  fseqenlem2  9790  dfac8alem  9794  ac5num  9801  acni2  9811  dfac4  9887  dfac2a  9894  dfacacn  9906  dfac12lem1  9908  ackbij1lem7  9991  ackbij2lem2  10005  ackbij2lem3  10006  cfsmolem  10035  fin23lem28  10105  fin23lem39  10115  isf32lem6  10123  isf32lem7  10124  isf32lem8  10125  fin1a2lem3  10167  itunifval  10181  itunisuc  10184  axdc2lem  10213  axdc3lem2  10216  axcclem  10222  zorn2lem1  10261  negiso  11964  infrenegsup  11967  uzval  12593  flval  13523  ceilval  13567  ceilval2  13569  monoord2  13763  seqf1olem2  13772  seqf1o  13773  seqdistr  13783  serle  13787  seqof  13789  swrdfv  14370  revval  14482  revfv  14485  wwlktovf1  14681  wwlktovfo  14682  sgnval  14808  cjval  14822  reval  14826  imval  14827  sqrtval  14957  absval  14958  limsupval  15192  limsupgval  15194  climmpt  15289  climle  15358  rlimdiv  15366  isercolllem1  15385  isercoll2  15389  caurcvg2  15398  fsumser  15451  isumadd  15488  fsumcnv  15494  fsumrev  15500  fsumshft  15501  iserabs  15536  cvgcmp  15537  cvgcmpce  15539  incexclem  15557  isumless  15566  divcnvshft  15576  supcvg  15577  harmonic  15580  trireciplem  15583  trirecip  15584  expcnv  15585  explecnv  15586  geolim  15591  geolim2  15592  geo2lim  15596  geomulcvg  15597  geoisum  15598  geoisumr  15599  geoisum1  15600  geoisum1c  15601  cvgrat  15604  mertenslem2  15606  mertens  15607  prodfdiv  15617  fprodser  15668  fprodshft  15695  fprodrev  15696  fprodcnv  15702  iprodmul  15722  bpolylem  15767  eftval  15795  efval  15798  efcvgfsum  15804  ege2le3  15808  eftlub  15827  eflegeo  15839  sinval  15840  cosval  15841  tanval  15846  eirrlem  15922  rpnnen2lem1  15932  rpnnen2lem2  15933  bitsfval  16139  bitsinv2  16159  bitsinv  16164  sadcf  16169  sadc0  16170  sadcp1  16171  smupf  16194  smup0  16195  smupp1  16196  qnumval  16450  qdenval  16451  phival  16477  crth  16488  phimullem  16489  eulerthlem2  16492  phisum  16500  odzval  16501  iserodd  16545  pcmpt  16602  prmreclem1  16626  prmreclem2  16627  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  1arithlem1  16633  1arithlem2  16634  vdwapfval  16681  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  vdwlem9  16699  ramub1lem2  16737  ramcl  16739  prmoval  16743  strfvnd  16895  topnval  17154  prdsplusgfval  17194  prdsmulrfval  17196  isacs  17369  acsfn  17377  homffval  17408  comfffval  17416  oppcval  17431  monfval  17453  oppcmon  17459  sectffval  17471  invffval  17479  isoval  17486  idfuval  17600  homafval  17753  arwval  17767  coafval  17788  yonedainv  18008  oduval  18015  pltfval  18058  lubfval  18077  lubval  18083  glbfval  18090  glbval  18096  p0val  18154  p1val  18155  ipoval  18257  plusffval  18341  grpidval  18354  issubm  18451  prdspjmhm  18476  efmnd  18518  smndex1igid  18552  grpinvfval  18627  grpinvval  18629  grpsubfval  18632  grpsubfvalALT  18633  grplactval  18686  prdsinvlem  18693  mulgfval  18711  mulgfvalALT  18712  pwsmulg  18757  issubg  18764  isnsg  18792  cycsubmel  18828  cycsubgcl  18834  conjghm  18874  conjnmz  18877  cntrval  18934  cntzfval  18935  cntzval  18936  oppgval  18960  psgnfval  19117  psgnval  19124  odfval  19149  odval  19151  sylow1lem4  19215  pgpssslw  19228  sylow2blem3  19236  sylow3lem2  19242  lsmfval  19252  pj1fval  19309  efgval  19332  efgsval  19346  frgpval  19373  vrgpval  19382  mulgmhm  19438  mulgghm  19439  ablfaclem1  19697  mgpval  19732  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  opprval  19872  dvdsrval  19896  isunit  19908  invrfval  19924  dvrfval  19935  isirred  19950  issubrg  20033  issdrg  20072  abvfval  20087  abvtrivd  20109  staffval  20116  stafval  20117  scaffval  20150  lmodvsghm  20193  lssset  20204  lspfval  20244  islbs  20347  sraval  20447  rlmval  20470  2idlval  20513  lpival  20525  rrgval  20567  fidomndrnglem  20587  expmhm  20676  expghm  20706  mulgghm2  20707  mulgrhm  20708  zrhval  20718  zrhmulg  20720  zlmval  20726  chrval  20738  znval  20748  znzrhval  20763  evpmss  20800  psgnevpmb  20801  ip0l  20850  ipffval  20862  ocvfval  20880  ocvval  20881  cssval  20896  thlval  20909  pjfval  20922  pjval  20926  isobs  20936  prdsinvgd2  20958  uvcresum  21009  frlmup1  21014  frlmup2  21015  islinds  21025  islindf5  21055  aspval  21086  asclval  21093  psrmulval  21164  psrlidm  21181  psrridm  21182  mvrval  21199  mvrval2  21200  mplmonmul  21246  evlslem3  21299  evlslem1  21301  evlsval  21305  evlssca  21308  evlsvar  21309  psr1val  21366  vr1val  21372  ply1val  21374  coe1fval  21385  coe1fv  21386  coe1tmmul2  21456  coe1tmmul  21457  coe1tmmul2fv  21458  coe1pwmulfv  21460  evls1val  21495  evl1fval  21503  evl1val  21504  mamulid  21599  mamurid  21600  mdetleib  21745  mdetleib1  21749  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  cpmidpmatlem1  22028  ordtval  22349  cnpval  22396  ptpjpre1  22731  ptpjopn  22772  dfac14  22778  upxp  22783  uptx  22785  hauseqlcld  22806  txlm  22808  xkoptsub  22814  xkoinjcn  22847  kqval  22886  xpstopnlem1  22969  fmval  23103  flfval  23150  ptcmplem2  23213  ptcmplem3  23214  symgtgp  23266  qustgpopn  23280  ussval  23420  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  mopnval  23600  prdsxmslem2  23694  nmfval  23753  nmval  23754  nmoval  23888  metdsval  24019  divcn  24040  mulc1cncf  24077  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  cnheiborlem  24126  evth  24131  evth2  24132  lebnumlem3  24135  isphtpy  24153  isphtpc  24166  pcofval  24182  pcovalg  24184  pco1  24187  pcopt  24194  pcopt2  24195  pcoass  24196  pcorevcl  24197  pcorevlem  24198  pcorev2  24200  pi1xfrcnv  24229  cphnm  24366  tcphval  24391  tcphnmval  24402  cfilfval  24437  iscmet  24457  iscmet3lem3  24463  rrxval  24560  ehlval  24587  ivth2  24628  ovolval  24646  ovollb2lem  24661  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliunlem2  24676  ovolicc1  24689  voliunlem1  24723  voliunlem2  24724  voliunlem3  24725  volsup  24729  ioorval  24747  uniioombllem3  24758  uniioombllem6  24761  volsup2  24778  volcn  24779  volivth  24780  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  vitali  24786  mbfmax  24822  mbfimaopnlem  24828  itg1val  24856  i1f1lem  24862  itg11  24864  itg1addlem4  24872  itg1addlem4OLD  24873  itg1mulc  24878  i1fres  24879  itg1climres  24888  mbfi1fseqlem2  24890  mbfi1fseqlem3  24891  mbfi1fseqlem6  24894  mbfi1flimlem  24896  mbfi1flim  24897  mbfmullem2  24898  itg2seq  24916  itg2uba  24917  itg2splitlem  24922  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  itg2cnlem1  24935  itg2cn  24937  limccnp2  25065  dvnff  25096  dvnp1  25098  cpnfval  25105  elcpn  25107  dvrec  25128  dvcnvlem  25149  dveflem  25152  dvef  25153  dvferm1  25158  dvferm2  25160  rolle  25163  dvlip  25166  dvlipcn  25167  dv11cn  25174  dvivthlem1  25181  dvivth  25183  lhop1lem  25186  ftc1lem1  25208  ftc1lem5  25213  ftc2  25217  itgsubstlem  25221  tdeglem3  25231  tdeglem3OLD  25232  tdeglem4  25233  tdeglem4OLD  25234  mdegval  25237  mdegmullem  25252  deg1fval  25254  deg1ldg  25266  deg1leb  25269  coe1mul3  25273  uc1pval  25313  mon1pval  25315  q1pval  25327  r1pval  25330  ply1remlem  25336  ig1pval  25346  plyval  25363  elply2  25366  plyeq0lem  25380  coeval  25393  dgrval  25398  coeid2  25409  coemullem  25420  coemul  25422  elqaalem1  25488  elqaalem2  25489  elqaalem3  25490  iaa  25494  aareccl  25495  aannenlem1  25497  geolim3  25508  aaliou3lem1  25511  aaliou3lem2  25512  aaliou3lem5  25516  aaliou3lem6  25517  aaliou3lem7  25518  aaliou3  25520  tayl0  25530  taylthlem1  25541  taylthlem2  25542  ulmshftlem  25557  ulmshft  25558  ulmuni  25560  ulmcau  25563  ulmdvlem1  25568  ulmdvlem3  25570  mtest  25572  mtestbdd  25573  mbfulm  25574  iblulm  25575  itgulm  25576  pserval  25578  pserval2  25579  radcnvlem1  25581  radcnvlem2  25582  dvradcnv  25589  pserulm  25590  pserdvlem2  25596  pserdv  25597  abelthlem1  25599  abelthlem3  25601  abelthlem4  25602  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  resinf1o  25701  efif1olem4  25710  eff1olem  25713  logcnlem5  25810  logtayllem  25823  logtayl  25824  logtaylsum  25825  logtayl2  25826  logccv  25827  asinval  26041  acosval  26042  atanval  26043  atantayl  26096  leibpilem2  26100  leibpi  26101  leibpisum  26102  log2cnv  26103  log2tlbnd  26104  areaval  26123  efrlim  26128  dfef2  26129  amgmlem  26148  emcllem2  26155  emcllem3  26156  emcllem4  26157  emcllem5  26158  emcllem6  26159  emcllem7  26160  zetacvg  26173  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulm2  26194  lgamcvglem  26198  igamval  26205  lgamcvg2  26213  gamcvg2lem  26217  ftalem7  26237  basellem2  26240  basellem3  26241  basellem4  26242  basellem5  26243  basellem6  26244  basellem8  26246  basellem9  26247  chtval  26268  vmaval  26271  chpval  26280  ppival  26285  muval  26290  prmorcht  26336  sqff1o  26340  dvdsflsumcom  26346  musum  26349  muinv  26351  sgmppw  26354  fsumvma  26370  pclogsum  26372  dchrfi  26412  bposlem5  26445  bposlem7  26447  bposlem8  26448  bposlem9  26449  lgsfval  26459  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgsqrlem2  26504  lgsqrlem4  26506  lgseisenlem2  26533  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasumiflem1  26658  dchrvmaeq0  26661  dchrisum0fval  26662  dchrisum0re  26670  mulog2sumlem1  26691  pntrval  26719  pntsval  26729  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntlem3  26766  abvcxp  26772  padicfval  26773  padicval  26774  padicabv  26787  ostth1  26790  ostth2  26794  ostth3  26795  iscgrg  26882  legval  26954  ishpg  27129  iscgra  27179  isinag  27208  isleag  27217  iseqlg  27237  ttgval  27245  ttgvalOLD  27246  elee  27271  axsegconlem1  27294  axsegconlem9  27302  axsegconlem10  27303  axpasch  27318  axlowdimlem15  27333  axlowdim  27338  axeuclidlem  27339  axcontlem2  27342  eengv  27356  vtxval  27379  iedgval  27380  edgval  27428  vtxdgval  27844  wwlksnextinj  28273  wwlksnextsurj  28274  clwwlkfv  28421  clwwlknonmpo  28462  fusgreg2wsplem  28706  fusgreghash2wsp  28711  numclwwlk1lem2fv  28729  gidval  28883  grpoinvval  28894  bafval  28975  imsval  29056  dipfval  29073  sspval  29094  nmooval  29134  hmoval  29181  ipasslem8  29208  ipasslem9  29209  ipblnfi  29226  ubthlem2  29242  htthlem  29288  normval  29495  ocval  29651  occllem  29674  hsupval  29705  pjhfval  29767  pjhval  29768  chscllem2  30009  chscllem3  30010  hosval  30111  homval  30112  hodval  30113  hfsval  30114  hfmval  30115  brafval  30314  braval  30315  kbval  30325  eigvalval  30331  cnlnadjlem1  30438  nmopadjlei  30459  hmopidmchi  30522  strlem2  30622  hstrlem2  30630  cdj3lem2  30806  ofpreima  31011  psgnfzto1stlem  31376  evpmval  31421  altgnsg  31425  inftmrel  31443  isinftm  31444  qusker  31558  qusvscpbl  31560  qusscaval  31561  mxidlval  31642  idlsrgval  31657  dimval  31695  dimvalfi  31696  smatfval  31754  lmatval  31772  locfinreflem  31799  rspecval  31823  rmulccn  31887  xrmulc1cn  31889  xrge0iifcv  31893  xrge0iifiso  31894  xrge0iifhom  31896  xrge0iif1  31897  qqhval  31933  rrhval  31955  xrhval  31977  ddeval1  32211  ddeval0  32212  sxbrsigalem0  32247  sxbrsigalem3  32248  eulerpartlemgv  32349  rrvmbfm  32418  dstrvval  32446  coinflippv  32459  ballotlem2  32464  ballotlemfval  32465  ballotlemi  32476  ballotlemsval  32484  ballotlemrval  32493  ballotth  32513  plymulx  32536  signstfv  32551  signsvvfval  32566  derangval  33138  subfacval  33144  erdszelem3  33164  erdszelem9  33170  erdszelem10  33171  txpconn  33203  indispconn  33205  cvxpconn  33213  cvmlift2lem2  33275  cvmlift2lem3  33276  cvmlift2lem7  33280  cvmliftphtlem  33288  cvmlift3lem4  33293  snmlfval  33301  snmlval  33302  gonafv  33321  mvtval  33471  mrsubffval  33478  mrsubcv  33481  mrsubrn  33484  elmrsubrn  33491  msubffval  33494  mvhval  33505  mpstval  33506  mstaval  33515  mclsval  33534  mppsval  33543  sinccvglem  33639  circum  33641  divcnvlin  33707  iprodefisum  33716  iprodgam  33717  faclimlem1  33718  faclimlem2  33719  faclim  33721  iprodfac  33722  faclim2  33723  dfrdg2  33780  nosupfv  33918  noinffv  33933  newval  34048  leftval  34056  rightval  34057  findabrcl  34652  dnival  34660  bj-evalval  35255  bj-inftyexpitaudisj  35385  bj-inftyexpiinv  35388  bj-inftyexpidisj  35390  curfv  35766  finixpnum  35771  poimirlem16  35802  poimir  35819  broucube  35820  mblfinlem2  35824  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  itg2addnclem3  35839  ftc1cnnc  35858  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anc  35867  ftc2nc  35868  fvopabf4g  35888  sdclem2  35909  fdc  35912  lmclim2  35925  geomcau  35926  istotbnd  35936  isbnd  35947  prdsbnd2  35962  heiborlem6  35983  heiborlem7  35984  heiborlem8  35985  rrnval  35994  rrncmslem  35999  idlval  36180  pridlval  36200  maxidlval  36206  lshpset  36999  lsatset  37011  lcvfbr  37041  lflset  37080  lflnegcl  37096  lshpkrlem1  37131  lshpkrlem2  37132  lshpkrlem3  37133  ldualset  37146  cmtfvalN  37231  cvrfval  37289  pats  37306  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  pointsetN  37762  psubspset  37765  pmapval  37778  paddfval  37818  pclfvalN  37910  polfvalN  37925  polvalN  37926  psubclsetN  37957  watvalN  38014  lhpset  38016  lautset  38103  pautsetN  38119  ldilset  38130  ltrnset  38139  dilsetN  38174  trnsetN  38177  trlset  38182  trlval  38183  tgrpset  38766  tendoset  38780  tendo02  38808  erngset  38821  erngset-rN  38829  cdlemksv  38865  dvaset  39026  dvaplusgv  39031  diafval  39052  diaval  39053  dvhset  39102  cdlemm10N  39139  docafvalN  39143  djafvalN  39155  dibfval  39162  dibval  39163  dicfval  39196  dicval  39197  dihval  39253  dochfval  39371  djhfval  39418  dochfl1  39497  lpolsetN  39503  lcdval  39610  mapdhval  39745  hvmapfval  39780  hdmap1fval  39817  pwspjmhmmgpd  40274  pwsexpg  40275  mhphf  40292  prjspval  40449  isnacs  40533  mzpclval  40554  mzpsubst  40577  mzprename  40578  mzpcompact2lem  40580  eldiophb  40586  diophrw  40588  eldioph2  40591  diophin  40601  diophun  40602  diophren  40642  pell1qrval  40675  pell14qrval  40677  pell1234qrval  40679  pellfundval  40709  rmxypairf1o  40740  rmxyval  40744  mzpcong  40801  pw2f1ocnv  40866  dnnumch1  40876  dfac11  40894  hbtlem1  40955  hbtlem7  40957  elmnc  40968  dgraaval  40976  mpaaval  40983  itgoval  40993  rgspnval  41000  flcidc  41006  mendval  41015  mon1pid  41037  cytpval  41041  elcnvlem  41216  comptiunov2i  41321  dftrcl3  41335  trclfvcom  41338  cnvtrclfv  41339  cotrcltrcl  41340  trclimalb2  41341  trclfvdecomr  41343  dfrtrcl3  41348  dfrtrcl4  41353  clsk1indlem0  41658  clsk1indlem2  41659  clsk1indlem3  41660  clsk1indlem4  41661  clsk1indlem1  41662  k0004val  41767  lhe4.4ex1a  41954  addrfv  42094  subrfv  42095  mulvfv  42096  monoord2xrv  43031  sumnnodd  43178  liminfgval  43310  ioodvbdlimc2lem  43482  itgsin0pilem1  43498  stoweidlem55  43603  wallispilem1  43613  wallispilem2  43614  wallispilem4  43616  wallispi2lem1  43619  wallispi2lem2  43620  dirkerval  43639  fourierdlem2  43657  fourierdlem3  43658  fourierdlem29  43684  fourierdlem62  43716  fourierdlem80  43734  fourierdlem103  43757  fourierdlem104  43758  fourierswlem  43778  fouriersw  43779  iundjiunlem  44004  carageniuncllem2  44067  0ome  44074  hoidmv1le  44139  hoidmvlelem3  44142  smflimsuplem7  44370  iccpval  44878  fppr  45189  issubmgm  45354  bigoval  45906  ackval0  46037  ackval41a  46051  eenglngeehlnm  46096  prstcval  46356  mndtcval  46377  vsetrec  46419  onsetreclem1  46421  elpglem3  46429  sinhval-named  46449  coshval-named  46450  tanhval-named  46451  secval  46460  cscval  46461  cotval  46462  aacllem  46516