Theorem fvmpt 6770

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496   ↦ cmpt 5148  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fv 6365

This theorem is referenced by:  fvmptex  6784  fvmptrabfv  6801  mptfvmpt  6992  ofval  7420  caofinvl  7438  fvresex  7663  1stval  7693  2ndval  7694  reldm  7745  curry1val  7802  curry2val  7806  fsplitfpar  7816  fnwelem  7827  brtpos2  7900  onovuni  7981  tz7.44-1  8044  oasuc  8151  oesuclem  8152  omsuc  8153  onasuc  8155  onmsuc  8156  fvmptmap  8447  xpcomco  8609  unxpdomlem1  8724  unfilem2  8785  ordtypelem3  8986  ixpiunwdom  9057  inf3lema  9089  noinfep  9125  cantnfval  9133  cantnflem1d  9153  cantnflem1  9154  r1sucg  9200  r0weon  9440  infxpenc2lem1  9447  fseqenlem1  9452  fseqenlem2  9453  dfac8alem  9457  ac5num  9464  acni2  9474  dfac4  9550  dfac2a  9557  dfacacn  9569  dfac12lem1  9571  ackbij1lem7  9650  ackbij2lem2  9664  ackbij2lem3  9665  cfsmolem  9694  fin23lem28  9764  fin23lem39  9774  isf32lem6  9782  isf32lem7  9783  isf32lem8  9784  fin1a2lem3  9826  itunifval  9840  itunisuc  9843  axdc2lem  9872  axdc3lem2  9875  axcclem  9881  zorn2lem1  9920  negiso  11623  infrenegsup  11626  uzval  12248  flval  13167  ceilval  13211  ceilval2  13213  monoord2  13404  seqf1olem2  13413  seqf1o  13414  seqdistr  13424  serle  13428  seqof  13430  swrdfv  14012  revval  14124  revfv  14127  wwlktovf1  14323  wwlktovfo  14324  sgnval  14449  cjval  14463  reval  14467  imval  14468  sqrtval  14598  absval  14599  limsupval  14833  limsupgval  14835  climmpt  14930  climle  14998  rlimdiv  15004  isercolllem1  15023  isercoll2  15027  caurcvg2  15036  fsumser  15089  isumadd  15124  fsumcnv  15130  fsumrev  15136  fsumshft  15137  iserabs  15172  cvgcmp  15173  cvgcmpce  15175  incexclem  15193  isumless  15202  divcnvshft  15212  supcvg  15213  harmonic  15216  trireciplem  15219  trirecip  15220  expcnv  15221  explecnv  15222  geolim  15228  geolim2  15229  geo2lim  15233  geomulcvg  15234  geoisum  15235  geoisumr  15236  geoisum1  15237  geoisum1c  15238  cvgrat  15241  mertenslem2  15243  mertens  15244  prodfdiv  15254  fprodser  15305  fprodshft  15332  fprodrev  15333  fprodcnv  15339  iprodmul  15359  bpolylem  15404  eftval  15432  efval  15435  efcvgfsum  15441  ege2le3  15445  eftlub  15464  eflegeo  15476  sinval  15477  cosval  15478  tanval  15483  eirrlem  15559  rpnnen2lem1  15569  rpnnen2lem2  15570  bitsfval  15774  bitsinv2  15794  bitsinv  15799  sadcf  15804  sadc0  15805  sadcp1  15806  smupf  15829  smup0  15830  smupp1  15831  qnumval  16079  qdenval  16080  phival  16106  crth  16117  phimullem  16118  eulerthlem2  16121  phisum  16129  odzval  16130  iserodd  16174  pcmpt  16230  prmreclem1  16254  prmreclem2  16255  prmreclem4  16257  prmreclem5  16258  prmreclem6  16259  1arithlem1  16261  1arithlem2  16262  vdwapfval  16309  vdwlem2  16320  vdwlem6  16324  vdwlem8  16326  vdwlem9  16327  ramub1lem2  16365  ramcl  16367  prmoval  16371  strfvnd  16504  topnval  16710  prdsplusgfval  16749  prdsmulrfval  16751  isacs  16924  acsfn  16932  homffval  16962  comfffval  16970  oppcval  16985  monfval  17004  oppcmon  17010  sectffval  17022  invffval  17030  isoval  17037  idfuval  17148  homafval  17291  arwval  17305  coafval  17326  yonedainv  17533  pltfval  17571  lubfval  17590  lubval  17596  glbfval  17603  glbval  17609  p0val  17653  p1val  17654  oduval  17742  ipoval  17766  plusffval  17860  grpidval  17873  issubm  17970  prdspjmhm  17995  efmnd  18037  smndex1igid  18071  grpinvfval  18144  grpinvval  18146  grpsubfval  18149  grpsubfvalALT  18150  grplactval  18203  prdsinvlem  18210  mulgfval  18228  mulgfvalALT  18229  pwsmulg  18274  issubg  18281  isnsg  18309  cycsubmel  18345  cycsubgcl  18351  conjghm  18391  conjnmz  18394  cntrval  18451  cntzfval  18452  cntzval  18453  oppgval  18477  psgnfval  18630  psgnval  18637  odfval  18662  odval  18664  sylow1lem4  18728  pgpssslw  18741  sylow2blem3  18749  sylow3lem2  18755  lsmfval  18765  pj1fval  18822  efgval  18845  efgsval  18859  frgpval  18886  vrgpval  18895  mulgmhm  18950  mulgghm  18951  ablfaclem1  19209  mgpval  19244  srglmhm  19287  srgrmhm  19288  ringlghm  19356  ringrghm  19357  opprval  19376  dvdsrval  19397  isunit  19409  invrfval  19425  dvrfval  19436  isirred  19451  issubrg  19537  issdrg  19576  abvfval  19591  abvtrivd  19613  staffval  19620  stafval  19621  scaffval  19654  lmodvsghm  19697  lssset  19707  lspfval  19747  islbs  19850  sraval  19950  rlmval  19965  2idlval  20008  lpival  20020  rrgval  20062  fidomndrnglem  20081  aspval  20104  asclval  20111  psrmulval  20168  psrlidm  20185  psrridm  20186  mvrval  20203  mvrval2  20204  mplmonmul  20247  evlslem3  20295  evlslem1  20297  evlsval  20301  evlssca  20304  evlsvar  20305  psr1val  20356  vr1val  20362  ply1val  20364  coe1fval  20375  coe1fv  20376  coe1tmmul2  20446  coe1tmmul  20447  coe1tmmul2fv  20448  coe1pwmulfv  20450  evls1val  20485  evl1fval  20493  evl1val  20494  expmhm  20616  expghm  20645  mulgghm2  20646  mulgrhm  20647  zrhval  20657  zrhmulg  20659  zlmval  20665  chrval  20674  znval  20684  znzrhval  20695  evpmss  20732  psgnevpmb  20733  ip0l  20782  ipffval  20794  ocvfval  20812  ocvval  20813  cssval  20828  thlval  20841  pjfval  20852  pjval  20856  isobs  20866  prdsinvgd2  20888  uvcresum  20939  frlmup1  20944  frlmup2  20945  islinds  20955  islindf5  20985  mamulid  21052  mamurid  21053  mdetleib  21198  mdetleib1  21202  mdetunilem9  21231  mdetuni0  21232  mdetmul  21234  cpmidpmatlem1  21480  ordtval  21799  cnpval  21846  ptpjpre1  22181  ptpjopn  22222  dfac14  22228  upxp  22233  uptx  22235  hauseqlcld  22256  txlm  22258  xkoptsub  22264  xkoinjcn  22297  kqval  22336  xpstopnlem1  22419  fmval  22553  flfval  22600  ptcmplem2  22663  ptcmplem3  22664  symgtgp  22716  qustgpopn  22730  ussval  22870  iscfilu  22899  ispsmet  22916  ismet  22935  isxmet  22936  mopnval  23050  prdsxmslem2  23141  nmfval  23200  nmval  23201  nmoval  23326  metdsval  23457  divcn  23478  mulc1cncf  23515  icopnfhmeo  23549  iccpnfhmeo  23551  xrhmeo  23552  cnheiborlem  23560  evth  23565  evth2  23566  lebnumlem3  23569  isphtpy  23587  isphtpc  23600  pcofval  23616  pcovalg  23618  pco1  23621  pcopt  23628  pcopt2  23629  pcoass  23630  pcorevcl  23631  pcorevlem  23632  pcorev2  23634  pi1xfrcnv  23663  cphnm  23799  tcphval  23823  tcphnmval  23834  cfilfval  23869  iscmet  23889  iscmet3lem3  23895  rrxval  23992  ehlval  24019  ivth2  24058  ovolval  24076  ovollb2lem  24091  ovolunlem1a  24099  ovolunlem1  24100  ovoliunlem1  24105  ovoliunlem2  24106  ovolicc1  24119  voliunlem1  24153  voliunlem2  24154  voliunlem3  24155  volsup  24159  ioorval  24177  uniioombllem3  24188  uniioombllem6  24191  volsup2  24208  volcn  24209  volivth  24210  vitalilem2  24212  vitalilem3  24213  vitalilem4  24214  vitali  24216  mbfmax  24252  mbfimaopnlem  24258  itg1val  24286  i1f1lem  24292  itg11  24294  itg1addlem4  24302  itg1mulc  24307  i1fres  24308  itg1climres  24317  mbfi1fseqlem2  24319  mbfi1fseqlem3  24320  mbfi1fseqlem6  24323  mbfi1flimlem  24325  mbfi1flim  24326  mbfmullem2  24327  itg2seq  24345  itg2uba  24346  itg2splitlem  24351  itg2monolem1  24353  itg2monolem2  24354  itg2monolem3  24355  itg2mono  24356  itg2i1fseqle  24357  itg2i1fseq  24358  itg2i1fseq2  24359  itg2addlem  24361  itg2cnlem1  24364  itg2cn  24366  limccnp2  24492  dvnff  24522  dvnp1  24524  cpnfval  24531  elcpn  24533  dvrec  24554  dvcnvlem  24575  dveflem  24578  dvef  24579  dvferm1  24584  dvferm2  24586  rolle  24589  dvlip  24592  dvlipcn  24593  dv11cn  24600  dvivthlem1  24607  dvivth  24609  lhop1lem  24612  ftc1lem1  24634  ftc1lem5  24639  ftc2  24643  itgsubstlem  24647  tdeglem3  24655  tdeglem4  24656  mdegval  24659  mdegmullem  24674  deg1fval  24676  deg1ldg  24688  deg1leb  24691  coe1mul3  24695  uc1pval  24735  mon1pval  24737  q1pval  24749  r1pval  24752  ply1remlem  24758  ig1pval  24768  plyval  24785  elply2  24788  plyeq0lem  24802  coeval  24815  dgrval  24820  coeid2  24831  coemullem  24842  coemul  24844  elqaalem1  24910  elqaalem2  24911  elqaalem3  24912  iaa  24916  aareccl  24917  aannenlem1  24919  geolim3  24930  aaliou3lem1  24933  aaliou3lem2  24934  aaliou3lem5  24938  aaliou3lem6  24939  aaliou3lem7  24940  aaliou3  24942  tayl0  24952  taylthlem1  24963  taylthlem2  24964  ulmshftlem  24979  ulmshft  24980  ulmuni  24982  ulmcau  24985  ulmdvlem1  24990  ulmdvlem3  24992  mtest  24994  mtestbdd  24995  mbfulm  24996  iblulm  24997  itgulm  24998  pserval  25000  pserval2  25001  radcnvlem1  25003  radcnvlem2  25004  dvradcnv  25011  pserulm  25012  pserdvlem2  25018  pserdv  25019  abelthlem1  25021  abelthlem3  25023  abelthlem4  25024  abelthlem5  25025  abelthlem6  25026  abelthlem7  25028  abelthlem8  25029  abelthlem9  25030  resinf1o  25122  efif1olem4  25131  eff1olem  25134  logcnlem5  25231  logtayllem  25244  logtayl  25245  logtaylsum  25246  logtayl2  25247  logccv  25248  asinval  25462  acosval  25463  atanval  25464  atantayl  25517  leibpilem2  25521  leibpi  25522  leibpisum  25523  log2cnv  25524  log2tlbnd  25525  areaval  25544  efrlim  25549  dfef2  25550  amgmlem  25569  emcllem2  25576  emcllem3  25577  emcllem4  25578  emcllem5  25579  emcllem6  25580  emcllem7  25581  zetacvg  25594  lgamgulmlem4  25611  lgamgulmlem5  25612  lgamgulm2  25615  lgamcvglem  25619  igamval  25626  lgamcvg2  25634  gamcvg2lem  25638  ftalem7  25658  basellem2  25661  basellem3  25662  basellem4  25663  basellem5  25664  basellem6  25665  basellem8  25667  basellem9  25668  chtval  25689  vmaval  25692  chpval  25701  ppival  25706  muval  25711  prmorcht  25757  sqff1o  25761  dvdsflsumcom  25767  musum  25770  muinv  25772  sgmppw  25775  fsumvma  25791  pclogsum  25793  dchrfi  25833  bposlem5  25866  bposlem7  25868  bposlem8  25869  bposlem9  25870  lgsfval  25880  lgsdir  25910  lgsdilem2  25911  lgsdi  25912  lgsne0  25913  lgsqrlem2  25925  lgsqrlem4  25927  lgseisenlem2  25954  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasumiflem1  26079  dchrvmaeq0  26082  dchrisum0fval  26083  dchrisum0re  26091  mulog2sumlem1  26112  pntrval  26140  pntsval  26150  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntlem3  26187  abvcxp  26193  padicfval  26194  padicval  26195  padicabv  26208  ostth1  26211  ostth2  26215  ostth3  26216  iscgrg  26300  legval  26372  ishpg  26547  iscgra  26597  isinag  26626  isleag  26635  iseqlg  26655  ttgval  26663  elee  26682  axsegconlem1  26705  axsegconlem9  26713  axsegconlem10  26714  axpasch  26729  axlowdimlem15  26744  axlowdim  26749  axeuclidlem  26750  axcontlem2  26753  eengv  26767  vtxval  26787  iedgval  26788  edgval  26836  vtxdgval  27252  wwlksnextinj  27679  wwlksnextsurj  27680  clwwlkfv  27829  clwwlknonmpo  27870  fusgreg2wsplem  28114  fusgreghash2wsp  28119  numclwwlk1lem2fv  28137  gidval  28291  grpoinvval  28302  bafval  28383  imsval  28464  dipfval  28481  sspval  28502  nmooval  28542  hmoval  28589  ipasslem8  28616  ipasslem9  28617  ipblnfi  28634  ubthlem2  28650  htthlem  28696  normval  28903  ocval  29059  occllem  29082  hsupval  29113  pjhfval  29175  pjhval  29176  chscllem2  29417  chscllem3  29418  hosval  29519  homval  29520  hodval  29521  hfsval  29522  hfmval  29523  brafval  29722  braval  29723  kbval  29733  eigvalval  29739  cnlnadjlem1  29846  nmopadjlei  29867  hmopidmchi  29930  strlem2  30030  hstrlem2  30038  cdj3lem2  30214  ofpreima  30412  psgnfzto1stlem  30744  evpmval  30789  altgnsg  30793  inftmrel  30811  isinftm  30812  qusker  30920  qusvscpbl  30922  qusscaval  30923  mxidlval  30972  dimval  31003  dimvalfi  31004  smatfval  31062  lmatval  31080  locfinreflem  31106  rmulccn  31173  xrmulc1cn  31175  xrge0iifcv  31179  xrge0iifiso  31180  xrge0iifhom  31182  xrge0iif1  31183  qqhval  31217  rrhval  31239  xrhval  31261  ddeval1  31495  ddeval0  31496  sxbrsigalem0  31531  sxbrsigalem3  31532  eulerpartlemgv  31633  rrvmbfm  31702  dstrvval  31730  coinflippv  31743  ballotlem2  31748  ballotlemfval  31749  ballotlemi  31760  ballotlemsval  31768  ballotlemrval  31777  ballotth  31797  plymulx  31820  signstfv  31835  signsvvfval  31850  derangval  32416  subfacval  32422  erdszelem3  32442  erdszelem9  32448  erdszelem10  32449  txpconn  32481  indispconn  32483  cvxpconn  32491  cvmlift2lem2  32553  cvmlift2lem3  32554  cvmlift2lem7  32558  cvmliftphtlem  32566  cvmlift3lem4  32571  snmlfval  32579  snmlval  32580  gonafv  32599  mvtval  32749  mrsubffval  32756  mrsubcv  32759  mrsubrn  32762  elmrsubrn  32769  msubffval  32772  mvhval  32783  mpstval  32784  mstaval  32793  mclsval  32812  mppsval  32821  sinccvglem  32917  circum  32919  divcnvlin  32966  iprodefisum  32975  iprodgam  32976  faclimlem1  32977  faclimlem2  32978  faclim  32980  iprodfac  32981  faclim2  32982  dfrdg2  33042  nosupfv  33208  findabrcl  33804  dnival  33812  bj-evalval  34368  bj-inftyexpitaudisj  34489  bj-inftyexpiinv  34492  bj-inftyexpidisj  34494  curfv  34874  finixpnum  34879  poimirlem16  34910  poimir  34927  broucube  34928  mblfinlem2  34932  voliunnfl  34938  volsupnfl  34939  itg2addnclem  34945  itg2addnclem3  34947  ftc1cnnc  34968  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anc  34977  ftc2nc  34978  fvopabf4g  34998  sdclem2  35019  fdc  35022  lmclim2  35035  geomcau  35036  istotbnd  35049  isbnd  35060  prdsbnd2  35075  heiborlem6  35096  heiborlem7  35097  heiborlem8  35098  rrnval  35107  rrncmslem  35112  idlval  35293  pridlval  35313  maxidlval  35319  lshpset  36116  lsatset  36128  lcvfbr  36158  lflset  36197  lflnegcl  36213  lshpkrlem1  36248  lshpkrlem2  36249  lshpkrlem3  36250  ldualset  36263  cmtfvalN  36348  cvrfval  36406  pats  36423  llnset  36643  lplnset  36667  lvolset  36710  lineset  36876  pointsetN  36879  psubspset  36882  pmapval  36895  paddfval  36935  pclfvalN  37027  polfvalN  37042  polvalN  37043  psubclsetN  37074  watvalN  37131  lhpset  37133  lautset  37220  pautsetN  37236  ldilset  37247  ltrnset  37256  dilsetN  37291  trnsetN  37294  trlset  37299  trlval  37300  tgrpset  37883  tendoset  37897  tendo02  37925  erngset  37938  erngset-rN  37946  cdlemksv  37982  dvaset  38143  dvaplusgv  38148  diafval  38169  diaval  38170  dvhset  38219  cdlemm10N  38256  docafvalN  38260  djafvalN  38272  dibfval  38279  dibval  38280  dicfval  38313  dicval  38314  dihval  38370  dochfval  38488  djhfval  38535  dochfl1  38614  lpolsetN  38620  lcdval  38727  mapdhval  38862  hvmapfval  38897  hdmap1fval  38934  prjspval  39260  isnacs  39308  mzpclval  39329  mzpsubst  39352  mzprename  39353  mzpcompact2lem  39355  eldiophb  39361  diophrw  39363  eldioph2  39366  diophin  39376  diophun  39377  diophren  39417  pell1qrval  39450  pell14qrval  39452  pell1234qrval  39454  pellfundval  39484  rmxypairf1o  39515  rmxyval  39519  mzpcong  39576  pw2f1ocnv  39641  dnnumch1  39651  dfac11  39669  hbtlem1  39730  hbtlem7  39732  elmnc  39743  dgraaval  39751  mpaaval  39758  itgoval  39768  rgspnval  39775  flcidc  39781  mendval  39790  mon1pid  39812  cytpval  39816  elcnvlem  39968  comptiunov2i  40058  dftrcl3  40072  trclfvcom  40075  cnvtrclfv  40076  cotrcltrcl  40077  trclimalb2  40078  trclfvdecomr  40080  dfrtrcl3  40085  dfrtrcl4  40090  clsk1indlem0  40398  clsk1indlem2  40399  clsk1indlem3  40400  clsk1indlem4  40401  clsk1indlem1  40402  k0004val  40507  lhe4.4ex1a  40668  addrfv  40808  subrfv  40809  mulvfv  40810  monoord2xrv  41767  sumnnodd  41918  liminfgval  42050  ioodvbdlimc2lem  42226  itgsin0pilem1  42242  stoweidlem55  42347  wallispilem1  42357  wallispilem2  42358  wallispilem4  42360  wallispi2lem1  42363  wallispi2lem2  42364  dirkerval  42383  fourierdlem2  42401  fourierdlem3  42402  fourierdlem29  42428  fourierdlem62  42460  fourierdlem80  42478  fourierdlem103  42501  fourierdlem104  42502  fourierswlem  42522  fouriersw  42523  iundjiunlem  42748  carageniuncllem2  42811  0ome  42818  hoidmv1le  42883  hoidmvlelem3  42886  smflimsuplem7  43107  iccpval  43582  fppr  43898  issubmgm  44063  bigoval  44616  eenglngeehlnm  44733  vsetrec  44812  onsetreclem1  44814  elpglem3  44822  sinhval-named  44842  coshval-named  44843  tanhval-named  44844  secval  44853  cscval  44854  cotval  44855  aacllem  44909