Theorem fvmpt 6999

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ↦ cmpt 5232  ‘cfv 6544

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552

This theorem is referenced by:  fvmptex  7013  fvmptrabfv  7030  mptfvmpt  7230  fvmptopab  7463  ofval  7681  caofinvl  7700  fvresex  7946  1stval  7977  2ndval  7978  reldm  8030  curry1val  8091  curry2val  8095  fsplitfpar  8104  fnwelem  8117  brtpos2  8217  onovuni  8342  tz7.44-1  8406  oasuc  8524  oesuclem  8525  omsuc  8526  onasuc  8528  onmsuc  8529  fvmptmap  8875  xpcomco  9062  unxpdomlem1  9250  unfilem2  9311  ordtypelem3  9515  ixpiunwdom  9585  inf3lema  9619  noinfep  9655  cantnfval  9663  cantnflem1d  9683  cantnflem1  9684  ssttrcl  9710  ttrcltr  9711  ttrclselem2  9721  r1sucg  9764  r0weon  10007  infxpenc2lem1  10014  fseqenlem1  10019  fseqenlem2  10020  dfac8alem  10024  ac5num  10031  acni2  10041  dfac4  10117  dfac2a  10124  dfacacn  10136  dfac12lem1  10138  ackbij1lem7  10221  ackbij2lem2  10235  ackbij2lem3  10236  cfsmolem  10265  fin23lem28  10335  fin23lem39  10345  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  fin1a2lem3  10397  itunifval  10411  itunisuc  10414  axdc2lem  10443  axdc3lem2  10446  axcclem  10452  zorn2lem1  10491  negiso  12194  infrenegsup  12197  uzval  12824  flval  13759  ceilval  13803  ceilval2  13805  monoord2  13999  seqf1olem2  14008  seqf1o  14009  seqdistr  14019  serle  14023  seqof  14025  swrdfv  14598  revval  14710  revfv  14713  wwlktovf1  14908  wwlktovfo  14909  sgnval  15035  cjval  15049  reval  15053  imval  15054  sqrtval  15184  absval  15185  limsupval  15418  limsupgval  15420  climmpt  15515  climle  15584  rlimdiv  15592  isercolllem1  15611  isercoll2  15615  caurcvg2  15624  fsumser  15676  isumadd  15713  fsumcnv  15719  fsumrev  15725  fsumshft  15726  iserabs  15761  cvgcmp  15762  cvgcmpce  15764  incexclem  15782  isumless  15791  divcnvshft  15801  supcvg  15802  harmonic  15805  trireciplem  15808  trirecip  15809  expcnv  15810  explecnv  15811  geolim  15816  geolim2  15817  geo2lim  15821  geomulcvg  15822  geoisum  15823  geoisumr  15824  geoisum1  15825  geoisum1c  15826  cvgrat  15829  mertenslem2  15831  mertens  15832  prodfdiv  15842  fprodser  15893  fprodshft  15920  fprodrev  15921  fprodcnv  15927  iprodmul  15947  bpolylem  15992  eftval  16020  efval  16023  efcvgfsum  16029  ege2le3  16033  eftlub  16052  eflegeo  16064  sinval  16065  cosval  16066  tanval  16071  eirrlem  16147  rpnnen2lem1  16157  rpnnen2lem2  16158  bitsfval  16364  bitsinv2  16384  bitsinv  16389  sadcf  16394  sadc0  16395  sadcp1  16396  smupf  16419  smup0  16420  smupp1  16421  qnumval  16673  qdenval  16674  phival  16700  crth  16711  phimullem  16712  eulerthlem2  16715  phisum  16723  odzval  16724  iserodd  16768  pcmpt  16825  prmreclem1  16849  prmreclem2  16850  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  1arithlem1  16856  1arithlem2  16857  vdwapfval  16904  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  ramub1lem2  16960  ramcl  16962  prmoval  16966  strfvnd  17118  topnval  17380  prdsplusgfval  17420  prdsmulrfval  17422  isacs  17595  acsfn  17603  homffval  17634  comfffval  17642  oppcval  17657  monfval  17679  oppcmon  17685  sectffval  17697  invffval  17705  isoval  17712  idfuval  17826  homafval  17979  arwval  17993  coafval  18014  yonedainv  18234  oduval  18241  pltfval  18284  lubfval  18303  lubval  18309  glbfval  18316  glbval  18322  p0val  18380  p1val  18381  ipoval  18483  plusffval  18567  grpidval  18580  issubm  18684  prdspjmhm  18710  efmnd  18751  smndex1igid  18785  grpinvfval  18863  grpinvval  18865  grpsubfval  18868  grpsubfvalALT  18869  grplactval  18925  prdsinvlem  18932  mulgfval  18952  mulgfvalALT  18953  pwsmulg  18999  issubg  19006  isnsg  19035  cycsubmel  19077  cycsubgcl  19083  conjghm  19123  conjnmz  19126  cntrval  19183  cntzfval  19184  cntzval  19185  oppgval  19211  psgnfval  19368  psgnval  19375  odfval  19400  odval  19402  sylow1lem4  19469  pgpssslw  19482  sylow2blem3  19490  sylow3lem2  19496  lsmfval  19506  pj1fval  19562  efgval  19585  efgsval  19599  frgpval  19626  vrgpval  19635  mulgmhm  19695  mulgghm  19696  ablfaclem1  19955  mgpval  19990  srglmhm  20044  srgrmhm  20045  ringlghm  20124  ringrghm  20125  pwspjmhmmgpd  20141  pwsexpg  20142  opprval  20151  dvdsrval  20175  isunit  20187  invrfval  20203  dvrfval  20216  isirred  20233  issubrg  20319  issdrg  20404  abvfval  20426  abvtrivd  20448  staffval  20455  stafval  20456  scaffval  20490  lmodvsghm  20533  lssset  20544  lspfval  20584  islbs  20687  sraval  20789  rlmval  20813  2idlval  20858  lpival  20883  rrgval  20903  fidomndrnglem  20925  expmhm  21014  expghm  21045  mulgghm2  21046  mulgrhm  21047  zrhval  21057  zrhmulg  21059  zlmval  21065  chrval  21077  znval  21087  znzrhval  21102  evpmss  21139  psgnevpmb  21140  ip0l  21189  ipffval  21201  ocvfval  21219  ocvval  21220  cssval  21235  thlval  21248  pjfval  21261  pjval  21265  isobs  21275  prdsinvgd2  21297  uvcresum  21348  frlmup1  21353  frlmup2  21354  islinds  21364  islindf5  21394  aspval  21427  asclval  21434  psrmulval  21505  psrlidm  21523  psrridm  21524  mvrval  21541  mvrval2  21542  mplmonmul  21591  evlslem3  21643  evlslem1  21645  evlsval  21649  evlssca  21652  evlsvar  21653  psr1val  21710  vr1val  21716  ply1val  21718  coe1fval  21729  coe1fv  21730  coe1tmmul2  21798  coe1tmmul  21799  coe1tmmul2fv  21800  coe1pwmulfv  21802  evls1val  21839  evl1fval  21847  evl1val  21848  mamulid  21943  mamurid  21944  mdetleib  22089  mdetleib1  22093  mdetunilem9  22122  mdetuni0  22123  mdetmul  22125  cpmidpmatlem1  22372  ordtval  22693  cnpval  22740  ptpjpre1  23075  ptpjopn  23116  dfac14  23122  upxp  23127  uptx  23129  hauseqlcld  23150  txlm  23152  xkoptsub  23158  xkoinjcn  23191  kqval  23230  xpstopnlem1  23313  fmval  23447  flfval  23494  ptcmplem2  23557  ptcmplem3  23558  symgtgp  23610  qustgpopn  23624  ussval  23764  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  mopnval  23944  prdsxmslem2  24038  nmfval  24097  nmval  24098  nmoval  24232  metdsval  24363  divcn  24384  mulc1cncf  24421  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  cnheiborlem  24470  evth  24475  evth2  24476  lebnumlem3  24479  isphtpy  24497  isphtpc  24510  pcofval  24526  pcovalg  24528  pco1  24531  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevcl  24541  pcorevlem  24542  pcorev2  24544  pi1xfrcnv  24573  cphnm  24710  tcphval  24735  tcphnmval  24746  cfilfval  24781  iscmet  24801  iscmet3lem3  24807  rrxval  24904  ehlval  24931  ivth2  24972  ovolval  24990  ovollb2lem  25005  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliunlem2  25020  ovolicc1  25033  voliunlem1  25067  voliunlem2  25068  voliunlem3  25069  volsup  25073  ioorval  25091  uniioombllem3  25102  uniioombllem6  25105  volsup2  25122  volcn  25123  volivth  25124  vitalilem2  25126  vitalilem3  25127  vitalilem4  25128  vitali  25130  mbfmax  25166  mbfimaopnlem  25172  itg1val  25200  i1f1lem  25206  itg11  25208  itg1addlem4  25216  itg1addlem4OLD  25217  itg1mulc  25222  i1fres  25223  itg1climres  25232  mbfi1fseqlem2  25234  mbfi1fseqlem3  25235  mbfi1fseqlem6  25238  mbfi1flimlem  25240  mbfi1flim  25241  mbfmullem2  25242  itg2seq  25260  itg2uba  25261  itg2splitlem  25266  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  itg2cnlem1  25279  itg2cn  25281  limccnp2  25409  dvnff  25440  dvnp1  25442  cpnfval  25449  elcpn  25451  dvrec  25472  dvcnvlem  25493  dveflem  25496  dvef  25497  dvferm1  25502  dvferm2  25504  rolle  25507  dvlip  25510  dvlipcn  25511  dv11cn  25518  dvivthlem1  25525  dvivth  25527  lhop1lem  25530  ftc1lem1  25552  ftc1lem5  25557  ftc2  25561  itgsubstlem  25565  tdeglem3  25575  tdeglem3OLD  25576  tdeglem4  25577  tdeglem4OLD  25578  mdegval  25581  mdegmullem  25596  deg1fval  25598  deg1ldg  25610  deg1leb  25613  coe1mul3  25617  uc1pval  25657  mon1pval  25659  q1pval  25671  r1pval  25674  ply1remlem  25680  ig1pval  25690  plyval  25707  elply2  25710  plyeq0lem  25724  coeval  25737  dgrval  25742  coeid2  25753  coemullem  25764  coemul  25766  elqaalem1  25832  elqaalem2  25833  elqaalem3  25834  iaa  25838  aareccl  25839  aannenlem1  25841  geolim3  25852  aaliou3lem1  25855  aaliou3lem2  25856  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  aaliou3  25864  tayl0  25874  taylthlem1  25885  taylthlem2  25886  ulmshftlem  25901  ulmshft  25902  ulmuni  25904  ulmcau  25907  ulmdvlem1  25912  ulmdvlem3  25914  mtest  25916  mtestbdd  25917  mbfulm  25918  iblulm  25919  itgulm  25920  pserval  25922  pserval2  25923  radcnvlem1  25925  radcnvlem2  25926  dvradcnv  25933  pserulm  25934  pserdvlem2  25940  pserdv  25941  abelthlem1  25943  abelthlem3  25945  abelthlem4  25946  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  abelthlem8  25951  abelthlem9  25952  resinf1o  26045  efif1olem4  26054  eff1olem  26057  logcnlem5  26154  logtayllem  26167  logtayl  26168  logtaylsum  26169  logtayl2  26170  logccv  26171  asinval  26387  acosval  26388  atanval  26389  atantayl  26442  leibpilem2  26446  leibpi  26447  leibpisum  26448  log2cnv  26449  log2tlbnd  26450  areaval  26469  efrlim  26474  dfef2  26475  amgmlem  26494  emcllem2  26501  emcllem3  26502  emcllem4  26503  emcllem5  26504  emcllem6  26505  emcllem7  26506  zetacvg  26519  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulm2  26540  lgamcvglem  26544  igamval  26551  lgamcvg2  26559  gamcvg2lem  26563  ftalem7  26583  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  basellem6  26590  basellem8  26592  basellem9  26593  chtval  26614  vmaval  26617  chpval  26626  ppival  26631  muval  26636  prmorcht  26682  sqff1o  26686  dvdsflsumcom  26692  musum  26695  muinv  26697  sgmppw  26700  fsumvma  26716  pclogsum  26718  dchrfi  26758  bposlem5  26791  bposlem7  26793  bposlem8  26794  bposlem9  26795  lgsfval  26805  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  lgsqrlem2  26850  lgsqrlem4  26852  lgseisenlem2  26879  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasumiflem1  27004  dchrvmaeq0  27007  dchrisum0fval  27008  dchrisum0re  27016  mulog2sumlem1  27037  pntrval  27065  pntsval  27075  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntlem3  27112  abvcxp  27118  padicfval  27119  padicval  27120  padicabv  27133  ostth1  27136  ostth2  27140  ostth3  27141  nosupfv  27209  noinffv  27224  newval  27350  leftval  27358  rightval  27359  iscgrg  27763  legval  27835  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  iseqlg  28118  ttgval  28126  ttgvalOLD  28127  elee  28152  axsegconlem1  28175  axsegconlem9  28183  axsegconlem10  28184  axpasch  28199  axlowdimlem15  28214  axlowdim  28219  axeuclidlem  28220  axcontlem2  28223  eengv  28237  vtxval  28260  iedgval  28261  edgval  28309  vtxdgval  28725  wwlksnextinj  29153  wwlksnextsurj  29154  clwwlkfv  29301  clwwlknonmpo  29342  fusgreg2wsplem  29586  fusgreghash2wsp  29591  numclwwlk1lem2fv  29609  gidval  29765  grpoinvval  29776  bafval  29857  imsval  29938  dipfval  29955  sspval  29976  nmooval  30016  hmoval  30063  ipasslem8  30090  ipasslem9  30091  ipblnfi  30108  ubthlem2  30124  htthlem  30170  normval  30377  ocval  30533  occllem  30556  hsupval  30587  pjhfval  30649  pjhval  30650  chscllem2  30891  chscllem3  30892  hosval  30993  homval  30994  hodval  30995  hfsval  30996  hfmval  30997  brafval  31196  braval  31197  kbval  31207  eigvalval  31213  cnlnadjlem1  31320  nmopadjlei  31341  hmopidmchi  31404  strlem2  31504  hstrlem2  31512  cdj3lem2  31688  ofpreima  31890  psgnfzto1stlem  32259  evpmval  32304  altgnsg  32308  inftmrel  32326  isinftm  32327  qusker  32464  qusvscpbl  32466  qusvsval  32467  mxidlval  32577  idlsrgval  32617  dimval  32686  dimvalfi  32687  smatfval  32775  lmatval  32793  locfinreflem  32820  rspecval  32844  rmulccn  32908  xrmulc1cn  32910  xrge0iifcv  32914  xrge0iifiso  32915  xrge0iifhom  32917  xrge0iif1  32918  qqhval  32954  rrhval  32976  xrhval  32998  ddeval1  33232  ddeval0  33233  sxbrsigalem0  33270  sxbrsigalem3  33271  eulerpartlemgv  33372  rrvmbfm  33441  dstrvval  33469  coinflippv  33482  ballotlem2  33487  ballotlemfval  33488  ballotlemi  33499  ballotlemsval  33507  ballotlemrval  33516  ballotth  33536  plymulx  33559  signstfv  33574  signsvvfval  33589  derangval  34158  subfacval  34164  erdszelem3  34184  erdszelem9  34190  erdszelem10  34191  txpconn  34223  indispconn  34225  cvxpconn  34233  cvmlift2lem2  34295  cvmlift2lem3  34296  cvmlift2lem7  34300  cvmliftphtlem  34308  cvmlift3lem4  34313  snmlfval  34321  snmlval  34322  gonafv  34341  mvtval  34491  mrsubffval  34498  mrsubcv  34501  mrsubrn  34504  elmrsubrn  34511  msubffval  34514  mvhval  34525  mpstval  34526  mstaval  34535  mclsval  34554  mppsval  34563  sinccvglem  34657  circum  34659  divcnvlin  34702  iprodefisum  34711  iprodgam  34712  faclimlem1  34713  faclimlem2  34714  faclim  34716  iprodfac  34717  faclim2  34718  dfrdg2  34767  gg-divcn  35163  gg-rmulccn  35179  findabrcl  35339  dnival  35347  bj-evalval  35956  bj-inftyexpitaudisj  36086  bj-inftyexpiinv  36089  bj-inftyexpidisj  36091  curfv  36468  finixpnum  36473  poimirlem16  36504  poimir  36521  broucube  36522  mblfinlem2  36526  voliunnfl  36532  volsupnfl  36533  itg2addnclem  36539  itg2addnclem3  36541  ftc1cnnc  36560  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anc  36569  ftc2nc  36570  fvopabf4g  36590  sdclem2  36610  fdc  36613  lmclim2  36626  geomcau  36627  istotbnd  36637  isbnd  36648  prdsbnd2  36663  heiborlem6  36684  heiborlem7  36685  heiborlem8  36686  rrnval  36695  rrncmslem  36700  idlval  36881  pridlval  36901  maxidlval  36907  lshpset  37848  lsatset  37860  lcvfbr  37890  lflset  37929  lflnegcl  37945  lshpkrlem1  37980  lshpkrlem2  37981  lshpkrlem3  37982  ldualset  37995  cmtfvalN  38080  cvrfval  38138  pats  38155  llnset  38376  lplnset  38400  lvolset  38443  lineset  38609  pointsetN  38612  psubspset  38615  pmapval  38628  paddfval  38668  pclfvalN  38760  polfvalN  38775  polvalN  38776  psubclsetN  38807  watvalN  38864  lhpset  38866  lautset  38953  pautsetN  38969  ldilset  38980  ltrnset  38989  dilsetN  39024  trnsetN  39027  trlset  39032  trlval  39033  tgrpset  39616  tendoset  39630  tendo02  39658  erngset  39671  erngset-rN  39679  cdlemksv  39715  dvaset  39876  dvaplusgv  39881  diafval  39902  diaval  39903  dvhset  39952  cdlemm10N  39989  docafvalN  39993  djafvalN  40005  dibfval  40012  dibval  40013  dicfval  40046  dicval  40047  dihval  40103  dochfval  40221  djhfval  40268  dochfl1  40347  lpolsetN  40353  lcdval  40460  mapdhval  40595  hvmapfval  40630  hdmap1fval  40667  prjspval  41345  isnacs  41442  mzpclval  41463  mzpsubst  41486  mzprename  41487  mzpcompact2lem  41489  eldiophb  41495  diophrw  41497  eldioph2  41500  diophin  41510  diophun  41511  diophren  41551  pell1qrval  41584  pell14qrval  41586  pell1234qrval  41588  pellfundval  41618  rmxypairf1o  41650  rmxyval  41654  mzpcong  41711  pw2f1ocnv  41776  dnnumch1  41786  dfac11  41804  hbtlem1  41865  hbtlem7  41867  elmnc  41878  dgraaval  41886  mpaaval  41893  itgoval  41903  rgspnval  41910  flcidc  41916  mendval  41925  mon1pid  41947  cytpval  41951  cantnfub  42071  cantnfresb  42074  tfsconcatrev  42098  elcnvlem  42352  comptiunov2i  42457  dftrcl3  42471  trclfvcom  42474  cnvtrclfv  42475  cotrcltrcl  42476  trclimalb2  42477  trclfvdecomr  42479  dfrtrcl3  42484  dfrtrcl4  42489  clsk1indlem0  42792  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem4  42795  clsk1indlem1  42796  k0004val  42901  lhe4.4ex1a  43088  addrfv  43228  subrfv  43229  mulvfv  43230  monoord2xrv  44194  sumnnodd  44346  liminfgval  44478  ioodvbdlimc2lem  44650  itgsin0pilem1  44666  stoweidlem55  44771  wallispilem1  44781  wallispilem2  44782  wallispilem4  44784  wallispi2lem1  44787  wallispi2lem2  44788  dirkerval  44807  fourierdlem2  44825  fourierdlem3  44826  fourierdlem29  44852  fourierdlem62  44884  fourierdlem80  44902  fourierdlem103  44925  fourierdlem104  44926  fourierswlem  44946  fouriersw  44947  iundjiunlem  45175  carageniuncllem2  45238  0ome  45245  hoidmv1le  45310  hoidmvlelem3  45313  smflimsuplem7  45542  iccpval  46083  fppr  46394  issubmgm  46559  issubrng  46726  bigoval  47235  ackval0  47366  ackval41a  47380  eenglngeehlnm  47425  prstcval  47684  mndtcval  47705  vsetrec  47748  onsetreclem1  47750  elpglem3  47758  pgindnf  47761  sinhval-named  47781  coshval-named  47782  tanhval-named  47783  secval  47792  cscval  47793  cotval  47794  aacllem  47848