Theorem fvmpt 6635

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  Vcvv 3437   ↦ cmpt 5041  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233

This theorem is referenced by:  fvmptex  6648  fvmptrabfv  6664  mptfvmpt  6856  ofval  7276  caofinvl  7294  fvresex  7517  1stval  7547  2ndval  7548  reldm  7599  curry1val  7656  curry2val  7660  fnwelem  7678  brtpos2  7749  onovuni  7831  tz7.44-1  7894  oasuc  8000  oesuclem  8001  omsuc  8002  onasuc  8004  onmsuc  8005  fvmptmap  8295  xpcomco  8454  unxpdomlem1  8568  unfilem2  8629  ordtypelem3  8830  ixpiunwdom  8901  inf3lema  8933  noinfep  8969  cantnfval  8977  cantnflem1d  8997  cantnflem1  8998  r1sucg  9044  r0weon  9284  infxpenc2lem1  9291  fseqenlem1  9296  fseqenlem2  9297  dfac8alem  9301  ac5num  9308  acni2  9318  dfac4  9394  dfac2a  9401  dfacacn  9413  dfac12lem1  9415  ackbij1lem7  9494  ackbij2lem2  9508  ackbij2lem3  9509  cfsmolem  9538  fin23lem28  9608  fin23lem39  9618  isf32lem6  9626  isf32lem7  9627  isf32lem8  9628  fin1a2lem3  9670  itunifval  9684  itunisuc  9687  axdc2lem  9716  axdc3lem2  9719  axcclem  9725  zorn2lem1  9764  negiso  11469  infrenegsup  11472  uzval  12095  flval  13014  ceilval  13058  ceilval2  13060  monoord2  13251  seqf1olem2  13260  seqf1o  13261  seqdistr  13271  serle  13275  seqof  13277  swrdfv  13846  revval  13958  revfv  13961  wwlktovf1  14155  wwlktovfo  14156  sgnval  14281  cjval  14295  reval  14299  imval  14300  sqrtval  14430  absval  14431  limsupval  14665  limsupgval  14667  climmpt  14762  climle  14830  rlimdiv  14836  isercolllem1  14855  isercoll2  14859  caurcvg2  14868  fsumser  14920  isumadd  14955  fsumcnv  14961  fsumrev  14967  fsumshft  14968  iserabs  15003  cvgcmp  15004  cvgcmpce  15006  incexclem  15024  isumless  15033  divcnvshft  15043  supcvg  15044  harmonic  15047  trireciplem  15050  trirecip  15051  expcnv  15052  explecnv  15053  geolim  15059  geolim2  15060  geo2lim  15064  geomulcvg  15065  geoisum  15066  geoisumr  15067  geoisum1  15068  geoisum1c  15069  cvgrat  15072  mertenslem2  15074  mertens  15075  prodfdiv  15085  fprodser  15136  fprodshft  15163  fprodrev  15164  fprodcnv  15170  iprodmul  15190  bpolylem  15235  eftval  15263  efval  15266  efcvgfsum  15272  ege2le3  15276  eftlub  15295  eflegeo  15307  sinval  15308  cosval  15309  tanval  15314  eirrlem  15390  rpnnen2lem1  15400  rpnnen2lem2  15401  bitsfval  15605  bitsinv2  15625  bitsinv  15630  sadcf  15635  sadc0  15636  sadcp1  15637  smupf  15660  smup0  15661  smupp1  15662  qnumval  15906  qdenval  15907  phival  15933  crth  15944  phimullem  15945  eulerthlem2  15948  phisum  15956  odzval  15957  iserodd  16001  pcmpt  16057  prmreclem1  16081  prmreclem2  16082  prmreclem4  16084  prmreclem5  16085  prmreclem6  16086  1arithlem1  16088  1arithlem2  16089  vdwapfval  16136  vdwlem2  16147  vdwlem6  16151  vdwlem8  16153  vdwlem9  16154  ramub1lem2  16192  ramcl  16194  prmoval  16198  strfvnd  16331  topnval  16537  prdsplusgfval  16576  prdsmulrfval  16578  isacs  16751  acsfn  16759  homffval  16789  comfffval  16797  oppcval  16812  monfval  16831  oppcmon  16837  sectffval  16849  invffval  16857  isoval  16864  idfuval  16975  homafval  17118  arwval  17132  coafval  17153  yonedainv  17360  pltfval  17398  lubfval  17417  lubval  17423  glbfval  17430  glbval  17436  p0val  17480  p1val  17481  oduval  17569  ipoval  17593  plusffval  17686  grpidval  17699  issubm  17786  prdspjmhm  17806  grpinvfval  17899  grpinvval  17901  grpsubfval  17904  grpsubfvalALT  17905  grplactval  17958  prdsinvlem  17965  mulgfval  17983  mulgfvalALT  17984  pwsmulg  18026  issubg  18033  cycsubgcl  18059  isnsg  18062  conjghm  18130  conjnmz  18133  cntrval  18190  cntzfval  18191  cntzval  18192  oppgval  18216  symgval  18238  psgnfval  18359  psgnval  18366  odfval  18391  odval  18393  sylow1lem4  18456  pgpssslw  18469  sylow2blem3  18477  sylow3lem2  18483  lsmfval  18493  pj1fval  18547  efgval  18570  efgsval  18584  frgpval  18611  vrgpval  18620  mulgmhm  18673  mulgghm  18674  ablfaclem1  18924  mgpval  18932  srglmhm  18975  srgrmhm  18976  ringlghm  19044  ringrghm  19045  opprval  19064  dvdsrval  19085  isunit  19097  invrfval  19113  dvrfval  19124  isirred  19139  issubrg  19225  issdrg  19264  abvfval  19279  abvtrivd  19301  staffval  19308  stafval  19309  scaffval  19342  lmodvsghm  19385  lssset  19395  lspfval  19435  islbs  19538  sraval  19638  rlmval  19653  2idlval  19695  lpival  19707  rrgval  19749  fidomndrnglem  19768  aspval  19790  asclval  19797  psrmulval  19854  psrlidm  19871  psrridm  19872  mvrval  19889  mvrval2  19890  mplmonmul  19932  evlslem3  19981  evlslem1  19982  evlsval  19986  evlssca  19989  evlsvar  19990  psr1val  20037  vr1val  20043  ply1val  20045  coe1fval  20056  coe1fv  20057  coe1tmmul2  20127  coe1tmmul  20128  coe1tmmul2fv  20129  coe1pwmulfv  20131  evls1val  20166  evl1fval  20173  evl1val  20174  expmhm  20296  expghm  20325  mulgghm2  20326  mulgrhm  20327  zrhval  20337  zrhmulg  20339  zlmval  20345  chrval  20354  znval  20364  znzrhval  20375  evpmss  20412  psgnevpmb  20413  ip0l  20462  ipffval  20474  ocvfval  20492  ocvval  20493  cssval  20508  thlval  20521  pjfval  20532  pjval  20536  isobs  20546  prdsinvgd2  20568  uvcresum  20619  frlmup1  20624  frlmup2  20625  islinds  20635  islindf5  20665  mamulid  20734  mamurid  20735  mdetleib  20880  mdetleib1  20884  mdetunilem9  20913  mdetuni0  20914  mdetmul  20916  cpmidpmatlem1  21162  ordtval  21481  cnpval  21528  ptpjpre1  21863  ptpjopn  21904  dfac14  21910  upxp  21915  uptx  21917  hauseqlcld  21938  txlm  21940  xkoptsub  21946  xkoinjcn  21979  kqval  22018  xpstopnlem1  22101  fmval  22235  flfval  22282  ptcmplem2  22345  ptcmplem3  22346  symgtgp  22393  qustgpopn  22411  ussval  22551  iscfilu  22580  ispsmet  22597  ismet  22616  isxmet  22617  mopnval  22731  prdsxmslem2  22822  nmfval  22881  nmval  22882  nmoval  23007  metdsval  23138  divcn  23159  mulc1cncf  23196  icopnfhmeo  23230  iccpnfhmeo  23232  xrhmeo  23233  cnheiborlem  23241  evth  23246  evth2  23247  lebnumlem3  23250  isphtpy  23268  isphtpc  23281  pcofval  23297  pcovalg  23299  pco1  23302  pcopt  23309  pcopt2  23310  pcoass  23311  pcorevcl  23312  pcorevlem  23313  pcorev2  23315  pi1xfrcnv  23344  cphnm  23480  tcphval  23504  tcphnmval  23515  cfilfval  23550  iscmet  23570  iscmet3lem3  23576  rrxval  23673  ehlval  23700  ivth2  23739  ovolval  23757  ovollb2lem  23772  ovolunlem1a  23780  ovolunlem1  23781  ovoliunlem1  23786  ovoliunlem2  23787  ovolicc1  23800  voliunlem1  23834  voliunlem2  23835  voliunlem3  23836  volsup  23840  ioorval  23858  uniioombllem3  23869  uniioombllem6  23872  volsup2  23889  volcn  23890  volivth  23891  vitalilem2  23893  vitalilem3  23894  vitalilem4  23895  vitali  23897  mbfmax  23933  mbfimaopnlem  23939  itg1val  23967  i1f1lem  23973  itg11  23975  itg1addlem4  23983  itg1mulc  23988  i1fres  23989  itg1climres  23998  mbfi1fseqlem2  24000  mbfi1fseqlem3  24001  mbfi1fseqlem6  24004  mbfi1flimlem  24006  mbfi1flim  24007  mbfmullem2  24008  itg2seq  24026  itg2uba  24027  itg2splitlem  24032  itg2monolem1  24034  itg2monolem2  24035  itg2monolem3  24036  itg2mono  24037  itg2i1fseqle  24038  itg2i1fseq  24039  itg2i1fseq2  24040  itg2addlem  24042  itg2cnlem1  24045  itg2cn  24047  limccnp2  24173  dvnff  24203  dvnp1  24205  cpnfval  24212  elcpn  24214  dvrec  24235  dvcnvlem  24256  dveflem  24259  dvef  24260  dvferm1  24265  dvferm2  24267  rolle  24270  dvlip  24273  dvlipcn  24274  dv11cn  24281  dvivthlem1  24288  dvivth  24290  lhop1lem  24293  ftc1lem1  24315  ftc1lem5  24320  ftc2  24324  itgsubstlem  24328  tdeglem3  24336  tdeglem4  24337  mdegval  24340  mdegmullem  24355  deg1fval  24357  deg1ldg  24369  deg1leb  24372  coe1mul3  24376  uc1pval  24416  mon1pval  24418  q1pval  24430  r1pval  24433  ply1remlem  24439  ig1pval  24449  plyval  24466  elply2  24469  plyeq0lem  24483  coeval  24496  dgrval  24501  coeid2  24512  coemullem  24523  coemul  24525  elqaalem1  24591  elqaalem2  24592  elqaalem3  24593  iaa  24597  aareccl  24598  aannenlem1  24600  geolim3  24611  aaliou3lem1  24614  aaliou3lem2  24615  aaliou3lem5  24619  aaliou3lem6  24620  aaliou3lem7  24621  aaliou3  24623  tayl0  24633  taylthlem1  24644  taylthlem2  24645  ulmshftlem  24660  ulmshft  24661  ulmuni  24663  ulmcau  24666  ulmdvlem1  24671  ulmdvlem3  24673  mtest  24675  mtestbdd  24676  mbfulm  24677  iblulm  24678  itgulm  24679  pserval  24681  pserval2  24682  radcnvlem1  24684  radcnvlem2  24685  dvradcnv  24692  pserulm  24693  pserdvlem2  24699  pserdv  24700  abelthlem1  24702  abelthlem3  24704  abelthlem4  24705  abelthlem5  24706  abelthlem6  24707  abelthlem7  24709  abelthlem8  24710  abelthlem9  24711  resinf1o  24801  efif1olem4  24810  eff1olem  24813  logcnlem5  24910  logtayllem  24923  logtayl  24924  logtaylsum  24925  logtayl2  24926  logccv  24927  asinval  25141  acosval  25142  atanval  25143  atantayl  25196  leibpilem2  25201  leibpi  25202  leibpisum  25203  log2cnv  25204  log2tlbnd  25205  areaval  25224  efrlim  25229  dfef2  25230  amgmlem  25249  emcllem2  25256  emcllem3  25257  emcllem4  25258  emcllem5  25259  emcllem6  25260  emcllem7  25261  zetacvg  25274  lgamgulmlem4  25291  lgamgulmlem5  25292  lgamgulm2  25295  lgamcvglem  25299  igamval  25306  lgamcvg2  25314  gamcvg2lem  25318  ftalem7  25338  basellem2  25341  basellem3  25342  basellem4  25343  basellem5  25344  basellem6  25345  basellem8  25347  basellem9  25348  chtval  25369  vmaval  25372  chpval  25381  ppival  25386  muval  25391  prmorcht  25437  sqff1o  25441  dvdsflsumcom  25447  musum  25450  muinv  25452  sgmppw  25455  fsumvma  25471  pclogsum  25473  dchrfi  25513  bposlem5  25546  bposlem7  25548  bposlem8  25549  bposlem9  25550  lgsfval  25560  lgsdir  25590  lgsdilem2  25591  lgsdi  25592  lgsne0  25593  lgsqrlem2  25605  lgsqrlem4  25607  lgseisenlem2  25634  dchrmusum2  25752  dchrvmasumlem1  25753  dchrvmasumiflem1  25759  dchrvmaeq0  25762  dchrisum0fval  25763  dchrisum0re  25771  mulog2sumlem1  25792  pntrval  25820  pntsval  25830  pntrlog2bndlem4  25838  pntrlog2bndlem5  25839  pntlem3  25867  abvcxp  25873  padicfval  25874  padicval  25875  padicabv  25888  ostth1  25891  ostth2  25895  ostth3  25896  iscgrg  25980  legval  26052  ishpg  26227  iscgra  26277  isinag  26307  isleag  26316  iseqlg  26336  ttgval  26344  elee  26363  axsegconlem1  26386  axsegconlem9  26394  axsegconlem10  26395  axpasch  26410  axlowdimlem15  26425  axlowdim  26430  axeuclidlem  26431  axcontlem2  26434  eengv  26448  vtxval  26468  iedgval  26469  edgval  26517  vtxdgval  26933  wwlksnextinj  27364  wwlksnextsurj  27365  clwwlkfv  27514  clwwlknonmpo  27555  fusgreg2wsplem  27804  fusgreghash2wsp  27809  numclwwlk1lem2fv  27827  gidval  27980  grpoinvval  27991  bafval  28072  imsval  28153  dipfval  28170  sspval  28191  nmooval  28231  hmoval  28278  ipasslem8  28305  ipasslem9  28306  ipblnfi  28323  ubthlem2  28339  htthlem  28385  normval  28592  ocval  28748  occllem  28771  hsupval  28802  pjhfval  28864  pjhval  28865  chscllem2  29106  chscllem3  29107  hosval  29208  homval  29209  hodval  29210  hfsval  29211  hfmval  29212  brafval  29411  braval  29412  kbval  29422  eigvalval  29428  cnlnadjlem1  29535  nmopadjlei  29556  hmopidmchi  29619  strlem2  29719  hstrlem2  29727  cdj3lem2  29903  ofpreima  30100  evpmval  30424  altgnsg  30429  inftmrel  30447  isinftm  30448  qusker  30572  qusvscpbl  30574  qusscaval  30575  dimval  30605  dimvalfi  30606  psgnfzto1stlem  30664  smatfval  30675  lmatval  30693  locfinreflem  30721  rmulccn  30788  xrmulc1cn  30790  xrge0iifcv  30794  xrge0iifiso  30795  xrge0iifhom  30797  xrge0iif1  30798  qqhval  30832  rrhval  30854  xrhval  30876  ddeval1  31110  ddeval0  31111  sxbrsigalem0  31146  sxbrsigalem3  31147  eulerpartlemgv  31248  rrvmbfm  31317  dstrvval  31345  coinflippv  31358  ballotlem2  31363  ballotlemfval  31364  ballotlemi  31375  ballotlemsval  31383  ballotlemrval  31392  ballotth  31412  plymulx  31435  signstfv  31450  signsvvfval  31465  derangval  32022  subfacval  32028  erdszelem3  32048  erdszelem9  32054  erdszelem10  32055  txpconn  32087  indispconn  32089  cvxpconn  32097  cvmlift2lem2  32159  cvmlift2lem3  32160  cvmlift2lem7  32164  cvmliftphtlem  32172  cvmlift3lem4  32177  snmlfval  32185  snmlval  32186  gonafv  32205  mvtval  32355  mrsubffval  32362  mrsubcv  32365  mrsubrn  32368  elmrsubrn  32375  msubffval  32378  mvhval  32389  mpstval  32390  mstaval  32399  mclsval  32418  mppsval  32427  sinccvglem  32523  circum  32525  divcnvlin  32572  iprodefisum  32581  iprodgam  32582  faclimlem1  32583  faclimlem2  32584  faclim  32586  iprodfac  32587  faclim2  32588  dfrdg2  32649  nosupfv  32815  findabrcl  33411  dnival  33419  bj-evalval  33964  bj-inftyexpitaudisj  34045  bj-inftyexpiinv  34048  bj-inftyexpidisj  34050  curfv  34403  finixpnum  34408  poimirlem16  34439  poimir  34456  broucube  34457  mblfinlem2  34461  voliunnfl  34467  volsupnfl  34468  itg2addnclem  34474  itg2addnclem3  34476  ftc1cnnc  34497  ftc1anclem5  34502  ftc1anclem6  34503  ftc1anclem7  34504  ftc1anc  34506  ftc2nc  34507  fvopabf4g  34528  sdclem2  34549  fdc  34552  lmclim2  34565  geomcau  34566  istotbnd  34579  isbnd  34590  prdsbnd2  34605  heiborlem6  34626  heiborlem7  34627  heiborlem8  34628  rrnval  34637  rrncmslem  34642  idlval  34823  pridlval  34843  maxidlval  34849  lshpset  35645  lsatset  35657  lcvfbr  35687  lflset  35726  lflnegcl  35742  lshpkrlem1  35777  lshpkrlem2  35778  lshpkrlem3  35779  ldualset  35792  cmtfvalN  35877  cvrfval  35935  pats  35952  llnset  36172  lplnset  36196  lvolset  36239  lineset  36405  pointsetN  36408  psubspset  36411  pmapval  36424  paddfval  36464  pclfvalN  36556  polfvalN  36571  polvalN  36572  psubclsetN  36603  watvalN  36660  lhpset  36662  lautset  36749  pautsetN  36765  ldilset  36776  ltrnset  36785  dilsetN  36820  trnsetN  36823  trlset  36828  trlval  36829  tgrpset  37412  tendoset  37426  tendo02  37454  erngset  37467  erngset-rN  37475  cdlemksv  37511  dvaset  37672  dvaplusgv  37677  diafval  37698  diaval  37699  dvhset  37748  cdlemm10N  37785  docafvalN  37789  djafvalN  37801  dibfval  37808  dibval  37809  dicfval  37842  dicval  37843  dihval  37899  dochfval  38017  djhfval  38064  dochfl1  38143  lpolsetN  38149  lcdval  38256  mapdhval  38391  hvmapfval  38426  hdmap1fval  38463  prjspval  38750  isnacs  38786  mzpclval  38807  mzpsubst  38830  mzprename  38831  mzpcompact2lem  38833  eldiophb  38839  diophrw  38841  eldioph2  38844  diophin  38854  diophun  38855  diophren  38895  pell1qrval  38928  pell14qrval  38930  pell1234qrval  38932  pellfundval  38962  rmxypairf1o  38993  rmxyval  38997  mzpcong  39054  pw2f1ocnv  39119  dnnumch1  39129  dfac11  39147  hbtlem1  39208  hbtlem7  39210  elmnc  39221  dgraaval  39229  mpaaval  39236  itgoval  39246  rgspnval  39253  flcidc  39259  mendval  39268  mon1pid  39290  cytpval  39294  elcnvlem  39446  comptiunov2i  39536  dftrcl3  39550  trclfvcom  39553  cnvtrclfv  39554  cotrcltrcl  39555  trclimalb2  39556  trclfvdecomr  39558  dfrtrcl3  39563  dfrtrcl4  39568  clsk1indlem0  39876  clsk1indlem2  39877  clsk1indlem3  39878  clsk1indlem4  39879  clsk1indlem1  39880  k0004val  39985  lhe4.4ex1a  40199  addrfv  40340  subrfv  40341  mulvfv  40342  monoord2xrv  41302  sumnnodd  41453  liminfgval  41585  ioodvbdlimc2lem  41760  itgsin0pilem1  41776  stoweidlem55  41882  wallispilem1  41892  wallispilem2  41893  wallispilem4  41895  wallispi2lem1  41898  wallispi2lem2  41899  dirkerval  41918  fourierdlem2  41936  fourierdlem3  41937  fourierdlem29  41963  fourierdlem62  41995  fourierdlem80  42013  fourierdlem103  42036  fourierdlem104  42037  fourierswlem  42057  fouriersw  42058  iundjiunlem  42283  carageniuncllem2  42346  0ome  42353  hoidmv1le  42418  hoidmvlelem3  42421  smflimsuplem7  42642  iccpval  43057  fppr  43373  issubmgm  43538  bigoval  44090  eenglngeehlnm  44207  vsetrec  44285  onsetreclem1  44287  elpglem3  44295  sinhval-named  44315  coshval-named  44316  tanhval-named  44317  secval  44326  cscval  44327  cotval  44328  aacllem  44382