Theorem fvmpt 6996

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

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

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 5299  ax-nul 5306  ax-pr 5427

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6493  df-fun 6543  df-fv 6549

This theorem is referenced by:  fvmptex  7010  fvmptrabfv  7027  mptfvmpt  7227  fvmptopab  7460  ofval  7678  caofinvl  7697  fvresex  7943  1stval  7974  2ndval  7975  reldm  8027  curry1val  8088  curry2val  8092  fsplitfpar  8101  fnwelem  8114  brtpos2  8214  onovuni  8339  tz7.44-1  8403  oasuc  8521  oesuclem  8522  omsuc  8523  onasuc  8525  onmsuc  8526  fvmptmap  8872  xpcomco  9059  unxpdomlem1  9247  unfilem2  9308  ordtypelem3  9512  ixpiunwdom  9582  inf3lema  9616  noinfep  9652  cantnfval  9660  cantnflem1d  9680  cantnflem1  9681  ssttrcl  9707  ttrcltr  9708  ttrclselem2  9718  r1sucg  9761  r0weon  10004  infxpenc2lem1  10011  fseqenlem1  10016  fseqenlem2  10017  dfac8alem  10021  ac5num  10028  acni2  10038  dfac4  10114  dfac2a  10121  dfacacn  10133  dfac12lem1  10135  ackbij1lem7  10218  ackbij2lem2  10232  ackbij2lem3  10233  cfsmolem  10262  fin23lem28  10332  fin23lem39  10342  isf32lem6  10350  isf32lem7  10351  isf32lem8  10352  fin1a2lem3  10394  itunifval  10408  itunisuc  10411  axdc2lem  10440  axdc3lem2  10443  axcclem  10449  zorn2lem1  10488  negiso  12191  infrenegsup  12194  uzval  12821  flval  13756  ceilval  13800  ceilval2  13802  monoord2  13996  seqf1olem2  14005  seqf1o  14006  seqdistr  14016  serle  14020  seqof  14022  swrdfv  14595  revval  14707  revfv  14710  wwlktovf1  14905  wwlktovfo  14906  sgnval  15032  cjval  15046  reval  15050  imval  15051  sqrtval  15181  absval  15182  limsupval  15415  limsupgval  15417  climmpt  15512  climle  15581  rlimdiv  15589  isercolllem1  15608  isercoll2  15612  caurcvg2  15621  fsumser  15673  isumadd  15710  fsumcnv  15716  fsumrev  15722  fsumshft  15723  iserabs  15758  cvgcmp  15759  cvgcmpce  15761  incexclem  15779  isumless  15788  divcnvshft  15798  supcvg  15799  harmonic  15802  trireciplem  15805  trirecip  15806  expcnv  15807  explecnv  15808  geolim  15813  geolim2  15814  geo2lim  15818  geomulcvg  15819  geoisum  15820  geoisumr  15821  geoisum1  15822  geoisum1c  15823  cvgrat  15826  mertenslem2  15828  mertens  15829  prodfdiv  15839  fprodser  15890  fprodshft  15917  fprodrev  15918  fprodcnv  15924  iprodmul  15944  bpolylem  15989  eftval  16017  efval  16020  efcvgfsum  16026  ege2le3  16030  eftlub  16049  eflegeo  16061  sinval  16062  cosval  16063  tanval  16068  eirrlem  16144  rpnnen2lem1  16154  rpnnen2lem2  16155  bitsfval  16361  bitsinv2  16381  bitsinv  16386  sadcf  16391  sadc0  16392  sadcp1  16393  smupf  16416  smup0  16417  smupp1  16418  qnumval  16670  qdenval  16671  phival  16697  crth  16708  phimullem  16709  eulerthlem2  16712  phisum  16720  odzval  16721  iserodd  16765  pcmpt  16822  prmreclem1  16846  prmreclem2  16847  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arithlem1  16853  1arithlem2  16854  vdwapfval  16901  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  ramub1lem2  16957  ramcl  16959  prmoval  16963  strfvnd  17115  topnval  17377  prdsplusgfval  17417  prdsmulrfval  17419  isacs  17592  acsfn  17600  homffval  17631  comfffval  17639  oppcval  17654  monfval  17676  oppcmon  17682  sectffval  17694  invffval  17702  isoval  17709  idfuval  17823  homafval  17976  arwval  17990  coafval  18011  yonedainv  18231  oduval  18238  pltfval  18281  lubfval  18300  lubval  18306  glbfval  18313  glbval  18319  p0val  18377  p1val  18378  ipoval  18480  plusffval  18564  grpidval  18577  issubm  18681  prdspjmhm  18707  efmnd  18748  smndex1igid  18782  grpinvfval  18860  grpinvval  18862  grpsubfval  18865  grpsubfvalALT  18866  grplactval  18922  prdsinvlem  18929  mulgfval  18947  mulgfvalALT  18948  pwsmulg  18994  issubg  19001  isnsg  19030  cycsubmel  19072  cycsubgcl  19078  conjghm  19118  conjnmz  19121  cntrval  19178  cntzfval  19179  cntzval  19180  oppgval  19206  psgnfval  19363  psgnval  19370  odfval  19395  odval  19397  sylow1lem4  19464  pgpssslw  19477  sylow2blem3  19485  sylow3lem2  19491  lsmfval  19501  pj1fval  19557  efgval  19580  efgsval  19594  frgpval  19621  vrgpval  19630  mulgmhm  19690  mulgghm  19691  ablfaclem1  19950  mgpval  19985  srglmhm  20038  srgrmhm  20039  ringlghm  20118  ringrghm  20119  pwspjmhmmgpd  20135  pwsexpg  20136  opprval  20144  dvdsrval  20168  isunit  20180  invrfval  20196  dvrfval  20209  isirred  20226  issubrg  20356  issdrg  20397  abvfval  20419  abvtrivd  20441  staffval  20448  stafval  20449  scaffval  20483  lmodvsghm  20526  lssset  20537  lspfval  20577  islbs  20680  sraval  20782  rlmval  20806  2idlval  20851  lpival  20876  rrgval  20896  fidomndrnglem  20918  expmhm  21007  expghm  21037  mulgghm2  21038  mulgrhm  21039  zrhval  21049  zrhmulg  21051  zlmval  21057  chrval  21069  znval  21079  znzrhval  21094  evpmss  21131  psgnevpmb  21132  ip0l  21181  ipffval  21193  ocvfval  21211  ocvval  21212  cssval  21227  thlval  21240  pjfval  21253  pjval  21257  isobs  21267  prdsinvgd2  21289  uvcresum  21340  frlmup1  21345  frlmup2  21346  islinds  21356  islindf5  21386  aspval  21419  asclval  21426  psrmulval  21497  psrlidm  21515  psrridm  21516  mvrval  21533  mvrval2  21534  mplmonmul  21583  evlslem3  21635  evlslem1  21637  evlsval  21641  evlssca  21644  evlsvar  21645  psr1val  21702  vr1val  21708  ply1val  21710  coe1fval  21721  coe1fv  21722  coe1tmmul2  21790  coe1tmmul  21791  coe1tmmul2fv  21792  coe1pwmulfv  21794  evls1val  21831  evl1fval  21839  evl1val  21840  mamulid  21935  mamurid  21936  mdetleib  22081  mdetleib1  22085  mdetunilem9  22114  mdetuni0  22115  mdetmul  22117  cpmidpmatlem1  22364  ordtval  22685  cnpval  22732  ptpjpre1  23067  ptpjopn  23108  dfac14  23114  upxp  23119  uptx  23121  hauseqlcld  23142  txlm  23144  xkoptsub  23150  xkoinjcn  23183  kqval  23222  xpstopnlem1  23305  fmval  23439  flfval  23486  ptcmplem2  23549  ptcmplem3  23550  symgtgp  23602  qustgpopn  23616  ussval  23756  iscfilu  23785  ispsmet  23802  ismet  23821  isxmet  23822  mopnval  23936  prdsxmslem2  24030  nmfval  24089  nmval  24090  nmoval  24224  metdsval  24355  divcn  24376  mulc1cncf  24413  icopnfhmeo  24451  iccpnfhmeo  24453  xrhmeo  24454  cnheiborlem  24462  evth  24467  evth2  24468  lebnumlem3  24471  isphtpy  24489  isphtpc  24502  pcofval  24518  pcovalg  24520  pco1  24523  pcopt  24530  pcopt2  24531  pcoass  24532  pcorevcl  24533  pcorevlem  24534  pcorev2  24536  pi1xfrcnv  24565  cphnm  24702  tcphval  24727  tcphnmval  24738  cfilfval  24773  iscmet  24793  iscmet3lem3  24799  rrxval  24896  ehlval  24923  ivth2  24964  ovolval  24982  ovollb2lem  24997  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliunlem2  25012  ovolicc1  25025  voliunlem1  25059  voliunlem2  25060  voliunlem3  25061  volsup  25065  ioorval  25083  uniioombllem3  25094  uniioombllem6  25097  volsup2  25114  volcn  25115  volivth  25116  vitalilem2  25118  vitalilem3  25119  vitalilem4  25120  vitali  25122  mbfmax  25158  mbfimaopnlem  25164  itg1val  25192  i1f1lem  25198  itg11  25200  itg1addlem4  25208  itg1addlem4OLD  25209  itg1mulc  25214  i1fres  25215  itg1climres  25224  mbfi1fseqlem2  25226  mbfi1fseqlem3  25227  mbfi1fseqlem6  25230  mbfi1flimlem  25232  mbfi1flim  25233  mbfmullem2  25234  itg2seq  25252  itg2uba  25253  itg2splitlem  25258  itg2monolem1  25260  itg2monolem2  25261  itg2monolem3  25262  itg2mono  25263  itg2i1fseqle  25264  itg2i1fseq  25265  itg2i1fseq2  25266  itg2addlem  25268  itg2cnlem1  25271  itg2cn  25273  limccnp2  25401  dvnff  25432  dvnp1  25434  cpnfval  25441  elcpn  25443  dvrec  25464  dvcnvlem  25485  dveflem  25488  dvef  25489  dvferm1  25494  dvferm2  25496  rolle  25499  dvlip  25502  dvlipcn  25503  dv11cn  25510  dvivthlem1  25517  dvivth  25519  lhop1lem  25522  ftc1lem1  25544  ftc1lem5  25549  ftc2  25553  itgsubstlem  25557  tdeglem3  25567  tdeglem3OLD  25568  tdeglem4  25569  tdeglem4OLD  25570  mdegval  25573  mdegmullem  25588  deg1fval  25590  deg1ldg  25602  deg1leb  25605  coe1mul3  25609  uc1pval  25649  mon1pval  25651  q1pval  25663  r1pval  25666  ply1remlem  25672  ig1pval  25682  plyval  25699  elply2  25702  plyeq0lem  25716  coeval  25729  dgrval  25734  coeid2  25745  coemullem  25756  coemul  25758  elqaalem1  25824  elqaalem2  25825  elqaalem3  25826  iaa  25830  aareccl  25831  aannenlem1  25833  geolim3  25844  aaliou3lem1  25847  aaliou3lem2  25848  aaliou3lem5  25852  aaliou3lem6  25853  aaliou3lem7  25854  aaliou3  25856  tayl0  25866  taylthlem1  25877  taylthlem2  25878  ulmshftlem  25893  ulmshft  25894  ulmuni  25896  ulmcau  25899  ulmdvlem1  25904  ulmdvlem3  25906  mtest  25908  mtestbdd  25909  mbfulm  25910  iblulm  25911  itgulm  25912  pserval  25914  pserval2  25915  radcnvlem1  25917  radcnvlem2  25918  dvradcnv  25925  pserulm  25926  pserdvlem2  25932  pserdv  25933  abelthlem1  25935  abelthlem3  25937  abelthlem4  25938  abelthlem5  25939  abelthlem6  25940  abelthlem7  25942  abelthlem8  25943  abelthlem9  25944  resinf1o  26037  efif1olem4  26046  eff1olem  26049  logcnlem5  26146  logtayllem  26159  logtayl  26160  logtaylsum  26161  logtayl2  26162  logccv  26163  asinval  26377  acosval  26378  atanval  26379  atantayl  26432  leibpilem2  26436  leibpi  26437  leibpisum  26438  log2cnv  26439  log2tlbnd  26440  areaval  26459  efrlim  26464  dfef2  26465  amgmlem  26484  emcllem2  26491  emcllem3  26492  emcllem4  26493  emcllem5  26494  emcllem6  26495  emcllem7  26496  zetacvg  26509  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulm2  26530  lgamcvglem  26534  igamval  26541  lgamcvg2  26549  gamcvg2lem  26553  ftalem7  26573  basellem2  26576  basellem3  26577  basellem4  26578  basellem5  26579  basellem6  26580  basellem8  26582  basellem9  26583  chtval  26604  vmaval  26607  chpval  26616  ppival  26621  muval  26626  prmorcht  26672  sqff1o  26676  dvdsflsumcom  26682  musum  26685  muinv  26687  sgmppw  26690  fsumvma  26706  pclogsum  26708  dchrfi  26748  bposlem5  26781  bposlem7  26783  bposlem8  26784  bposlem9  26785  lgsfval  26795  lgsdir  26825  lgsdilem2  26826  lgsdi  26827  lgsne0  26828  lgsqrlem2  26840  lgsqrlem4  26842  lgseisenlem2  26869  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasumiflem1  26994  dchrvmaeq0  26997  dchrisum0fval  26998  dchrisum0re  27006  mulog2sumlem1  27027  pntrval  27055  pntsval  27065  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntlem3  27102  abvcxp  27108  padicfval  27109  padicval  27110  padicabv  27123  ostth1  27126  ostth2  27130  ostth3  27131  nosupfv  27199  noinffv  27214  newval  27340  leftval  27348  rightval  27349  iscgrg  27753  legval  27825  ishpg  28000  iscgra  28050  isinag  28079  isleag  28088  iseqlg  28108  ttgval  28116  ttgvalOLD  28117  elee  28142  axsegconlem1  28165  axsegconlem9  28173  axsegconlem10  28174  axpasch  28189  axlowdimlem15  28204  axlowdim  28209  axeuclidlem  28210  axcontlem2  28213  eengv  28227  vtxval  28250  iedgval  28251  edgval  28299  vtxdgval  28715  wwlksnextinj  29143  wwlksnextsurj  29144  clwwlkfv  29291  clwwlknonmpo  29332  fusgreg2wsplem  29576  fusgreghash2wsp  29581  numclwwlk1lem2fv  29599  gidval  29753  grpoinvval  29764  bafval  29845  imsval  29926  dipfval  29943  sspval  29964  nmooval  30004  hmoval  30051  ipasslem8  30078  ipasslem9  30079  ipblnfi  30096  ubthlem2  30112  htthlem  30158  normval  30365  ocval  30521  occllem  30544  hsupval  30575  pjhfval  30637  pjhval  30638  chscllem2  30879  chscllem3  30880  hosval  30981  homval  30982  hodval  30983  hfsval  30984  hfmval  30985  brafval  31184  braval  31185  kbval  31195  eigvalval  31201  cnlnadjlem1  31308  nmopadjlei  31329  hmopidmchi  31392  strlem2  31492  hstrlem2  31500  cdj3lem2  31676  ofpreima  31878  psgnfzto1stlem  32247  evpmval  32292  altgnsg  32296  inftmrel  32314  isinftm  32315  qusker  32453  qusvscpbl  32455  qusvsval  32456  mxidlval  32566  idlsrgval  32606  dimval  32675  dimvalfi  32676  smatfval  32764  lmatval  32782  locfinreflem  32809  rspecval  32833  rmulccn  32897  xrmulc1cn  32899  xrge0iifcv  32903  xrge0iifiso  32904  xrge0iifhom  32906  xrge0iif1  32907  qqhval  32943  rrhval  32965  xrhval  32987  ddeval1  33221  ddeval0  33222  sxbrsigalem0  33259  sxbrsigalem3  33260  eulerpartlemgv  33361  rrvmbfm  33430  dstrvval  33458  coinflippv  33471  ballotlem2  33476  ballotlemfval  33477  ballotlemi  33488  ballotlemsval  33496  ballotlemrval  33505  ballotth  33525  plymulx  33548  signstfv  33563  signsvvfval  33578  derangval  34147  subfacval  34153  erdszelem3  34173  erdszelem9  34179  erdszelem10  34180  txpconn  34212  indispconn  34214  cvxpconn  34222  cvmlift2lem2  34284  cvmlift2lem3  34285  cvmlift2lem7  34289  cvmliftphtlem  34297  cvmlift3lem4  34302  snmlfval  34310  snmlval  34311  gonafv  34330  mvtval  34480  mrsubffval  34487  mrsubcv  34490  mrsubrn  34493  elmrsubrn  34500  msubffval  34503  mvhval  34514  mpstval  34515  mstaval  34524  mclsval  34543  mppsval  34552  sinccvglem  34646  circum  34648  divcnvlin  34691  iprodefisum  34700  iprodgam  34701  faclimlem1  34702  faclimlem2  34703  faclim  34705  iprodfac  34706  faclim2  34707  dfrdg2  34756  gg-divcn  35152  gg-rmulccn  35168  findabrcl  35328  dnival  35336  bj-evalval  35945  bj-inftyexpitaudisj  36075  bj-inftyexpiinv  36078  bj-inftyexpidisj  36080  curfv  36457  finixpnum  36462  poimirlem16  36493  poimir  36510  broucube  36511  mblfinlem2  36515  voliunnfl  36521  volsupnfl  36522  itg2addnclem  36528  itg2addnclem3  36530  ftc1cnnc  36549  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anc  36558  ftc2nc  36559  fvopabf4g  36579  sdclem2  36599  fdc  36602  lmclim2  36615  geomcau  36616  istotbnd  36626  isbnd  36637  prdsbnd2  36652  heiborlem6  36673  heiborlem7  36674  heiborlem8  36675  rrnval  36684  rrncmslem  36689  idlval  36870  pridlval  36890  maxidlval  36896  lshpset  37837  lsatset  37849  lcvfbr  37879  lflset  37918  lflnegcl  37934  lshpkrlem1  37969  lshpkrlem2  37970  lshpkrlem3  37971  ldualset  37984  cmtfvalN  38069  cvrfval  38127  pats  38144  llnset  38365  lplnset  38389  lvolset  38432  lineset  38598  pointsetN  38601  psubspset  38604  pmapval  38617  paddfval  38657  pclfvalN  38749  polfvalN  38764  polvalN  38765  psubclsetN  38796  watvalN  38853  lhpset  38855  lautset  38942  pautsetN  38958  ldilset  38969  ltrnset  38978  dilsetN  39013  trnsetN  39016  trlset  39021  trlval  39022  tgrpset  39605  tendoset  39619  tendo02  39647  erngset  39660  erngset-rN  39668  cdlemksv  39704  dvaset  39865  dvaplusgv  39870  diafval  39891  diaval  39892  dvhset  39941  cdlemm10N  39978  docafvalN  39982  djafvalN  39994  dibfval  40001  dibval  40002  dicfval  40035  dicval  40036  dihval  40092  dochfval  40210  djhfval  40257  dochfl1  40336  lpolsetN  40342  lcdval  40449  mapdhval  40584  hvmapfval  40619  hdmap1fval  40656  prjspval  41342  isnacs  41428  mzpclval  41449  mzpsubst  41472  mzprename  41473  mzpcompact2lem  41475  eldiophb  41481  diophrw  41483  eldioph2  41486  diophin  41496  diophun  41497  diophren  41537  pell1qrval  41570  pell14qrval  41572  pell1234qrval  41574  pellfundval  41604  rmxypairf1o  41636  rmxyval  41640  mzpcong  41697  pw2f1ocnv  41762  dnnumch1  41772  dfac11  41790  hbtlem1  41851  hbtlem7  41853  elmnc  41864  dgraaval  41872  mpaaval  41879  itgoval  41889  rgspnval  41896  flcidc  41902  mendval  41911  mon1pid  41933  cytpval  41937  cantnfub  42057  cantnfresb  42060  tfsconcatrev  42084  elcnvlem  42338  comptiunov2i  42443  dftrcl3  42457  trclfvcom  42460  cnvtrclfv  42461  cotrcltrcl  42462  trclimalb2  42463  trclfvdecomr  42465  dfrtrcl3  42470  dfrtrcl4  42475  clsk1indlem0  42778  clsk1indlem2  42779  clsk1indlem3  42780  clsk1indlem4  42781  clsk1indlem1  42782  k0004val  42887  lhe4.4ex1a  43074  addrfv  43214  subrfv  43215  mulvfv  43216  monoord2xrv  44181  sumnnodd  44333  liminfgval  44465  ioodvbdlimc2lem  44637  itgsin0pilem1  44653  stoweidlem55  44758  wallispilem1  44768  wallispilem2  44769  wallispilem4  44771  wallispi2lem1  44774  wallispi2lem2  44775  dirkerval  44794  fourierdlem2  44812  fourierdlem3  44813  fourierdlem29  44839  fourierdlem62  44871  fourierdlem80  44889  fourierdlem103  44912  fourierdlem104  44913  fourierswlem  44933  fouriersw  44934  iundjiunlem  45162  carageniuncllem2  45225  0ome  45232  hoidmv1le  45297  hoidmvlelem3  45300  smflimsuplem7  45529  iccpval  46070  fppr  46381  issubmgm  46546  issubrng  46711  bigoval  47189  ackval0  47320  ackval41a  47334  eenglngeehlnm  47379  prstcval  47638  mndtcval  47659  vsetrec  47702  onsetreclem1  47704  elpglem3  47712  pgindnf  47715  sinhval-named  47735  coshval-named  47736  tanhval-named  47737  secval  47746  cscval  47747  cotval  47748  aacllem  47802