Theorem fvmpt 6282

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)

Hypotheses

Ref	Expression
fvmptg.1	|- ( x = A -> B = C )
fvmptg.2	|- F = ( x e. D |-> B )
fvmpt.3	|- C e. _V

Assertion

Ref	Expression
fvmpt	|- ( A e. D -> ( F ` A ) = C )

Distinct variable groups:   x, A   x, C   x, D

Allowed substitution hints:   B( x)   F( x)

Proof of Theorem fvmpt

Step	Hyp	Ref	Expression
1		fvmpt.3	. 2 |- C e. _V
2		fvmptg.1	. . 3 |- ( x = A -> B = C )
3		fvmptg.2	. . 3 |- F = ( x e. D |-> B )
4	2, 3	fvmptg 6280	. 2 |- ( ( A e. D /\ C e. _V ) -> ( F ` A ) = C )
5	1, 4	mpan2 707	1 |- ( A e. D -> ( F ` A ) = C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   |-> cmpt 4729   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  fvmptex  6294  ofval  6906  caofinvl  6924  fvresex  7139  1stval  7170  2ndval  7171  reldm  7219  curry1val  7270  curry2val  7274  fnwelem  7292  brtpos2  7358  onovuni  7439  tz7.44-1  7502  oasuc  7604  oesuclem  7605  omsuc  7606  onasuc  7608  onmsuc  7609  fvmptmap  7894  xpcomco  8050  unxpdomlem1  8164  unfilem2  8225  ordtypelem3  8425  ixpiunwdom  8496  inf3lema  8521  noinfep  8557  cantnfval  8565  cantnflem1d  8585  cantnflem1  8586  r1sucg  8632  r0weon  8835  infxpenc2lem1  8842  fseqenlem1  8847  fseqenlem2  8848  dfac8alem  8852  ac5num  8859  acni2  8869  dfac4  8945  dfac2a  8952  dfacacn  8963  dfac12lem1  8965  ackbij1lem7  9048  ackbij2lem2  9062  ackbij2lem3  9063  cfsmolem  9092  fin23lem28  9162  fin23lem39  9172  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  fin1a2lem3  9224  itunifval  9238  itunisuc  9241  axdc2lem  9270  axdc3lem2  9273  axcclem  9279  zorn2lem1  9318  negiso  11003  infrenegsup  11006  uzval  11689  flval  12595  ceilval  12639  ceilval2  12641  monoord2  12832  seqf1olem2  12841  seqf1o  12842  seqdistr  12852  serle  12856  seqof  12858  swrdfv  13424  revval  13509  revfv  13512  wwlktovf1  13700  wwlktovfo  13701  sgnval  13828  cjval  13842  reval  13846  imval  13847  sqrtval  13977  absval  13978  limsupval  14205  limsupgval  14207  climmpt  14302  climle  14370  rlimdiv  14376  isercolllem1  14395  isercoll2  14399  caurcvg2  14408  fsumser  14461  isumadd  14498  fsumcnv  14504  fsumrev  14511  fsumshft  14512  iserabs  14547  cvgcmp  14548  cvgcmpce  14550  incexclem  14568  isumless  14577  divcnvshft  14587  supcvg  14588  harmonic  14591  trireciplem  14594  trirecip  14595  expcnv  14596  explecnv  14597  geolim  14601  geolim2  14602  geo2lim  14606  geomulcvg  14607  geoisum  14608  geoisumr  14609  geoisum1  14610  geoisum1c  14611  cvgrat  14615  mertenslem2  14617  mertens  14618  prodfdiv  14628  fprodser  14679  fprodshft  14706  fprodrev  14707  fprodcnv  14713  iprodmul  14734  bpolylem  14779  eftval  14807  efval  14810  efcvgfsum  14816  ege2le3  14820  eftlub  14839  eflegeo  14851  sinval  14852  cosval  14853  tanval  14858  eirrlem  14932  rpnnen2lem1  14943  rpnnen2lem2  14944  bitsfval  15145  bitsinv2  15165  bitsinv  15170  sadcf  15175  sadc0  15176  sadcp1  15177  smupf  15200  smup0  15201  smupp1  15202  qnumval  15445  qdenval  15446  phival  15472  crth  15483  phimullem  15484  eulerthlem2  15487  phisum  15495  odzval  15496  iserodd  15540  pcmpt  15596  prmreclem1  15620  prmreclem2  15621  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  1arithlem1  15627  1arithlem2  15628  vdwapfval  15675  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  ramub1lem2  15731  ramcl  15733  strfvnd  15876  topnval  16095  prdsplusgfval  16134  prdsmulrfval  16136  isacs  16312  acsfn  16320  cidfval  16337  homffval  16350  comfffval  16358  oppcval  16373  monfval  16392  oppcmon  16398  sectffval  16410  invffval  16418  isoval  16425  idfuval  16536  homafval  16679  arwval  16693  idafval  16707  coafval  16714  yonedainv  16921  pltfval  16959  lubfval  16978  lubval  16984  glbfval  16991  glbval  16997  p0val  17041  p1val  17042  oduval  17130  ipoval  17154  plusffval  17247  grpidval  17260  issubm  17347  prdspjmhm  17367  grpinvfval  17460  grpinvval  17461  grpsubfval  17464  grplactfval  17516  grplactval  17517  prdsinvlem  17524  mulgfval  17542  pwsmulg  17587  issubg  17594  cycsubgcl  17620  isnsg  17623  conjghm  17691  conjnmz  17694  cntrval  17752  cntzfval  17753  cntzval  17754  oppgval  17777  symgval  17799  psgnfval  17920  psgnval  17927  odfval  17952  odval  17953  sylow1lem4  18016  pgpssslw  18029  sylow2blem3  18037  sylow3lem2  18043  lsmfval  18053  pj1fval  18107  efgval  18130  efgsval  18144  frgpval  18171  vrgpval  18180  mulgmhm  18233  mulgghm  18234  ablfaclem1  18484  mgpval  18492  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  opprval  18624  dvdsrval  18645  isunit  18657  invrfval  18673  dvrfval  18684  isirred  18699  issubrg  18780  abvfval  18818  abvtrivd  18840  staffval  18847  stafval  18848  scaffval  18881  lmodvsghm  18924  lssset  18934  lspfval  18973  islbs  19076  sraval  19176  rlmval  19191  2idlval  19233  lpival  19245  rrgval  19287  fidomndrnglem  19306  aspval  19328  asclfval  19334  asclval  19335  psrmulval  19386  psrlidm  19403  psrridm  19404  mvrval  19421  mvrval2  19422  mplmonmul  19464  evlslem3  19514  evlslem1  19515  evlsval  19519  evlssca  19522  evlsvar  19523  psr1val  19556  vr1val  19562  ply1val  19564  coe1fval  19575  coe1fv  19576  coe1tmmul2  19646  coe1tmmul  19647  coe1tmmul2fv  19648  coe1pwmulfv  19650  evls1val  19685  evl1fval  19692  evl1val  19693  expmhm  19815  expghm  19844  mulgghm2  19845  mulgrhm  19846  zrhval  19856  zrhmulg  19858  zlmval  19864  chrval  19873  znval  19883  znzrhval  19895  evpmss  19932  psgnevpmb  19933  ip0l  19981  ipffval  19993  ocvfval  20010  ocvval  20011  cssval  20026  thlval  20039  pjfval  20050  pjval  20054  isobs  20064  prdsinvgd2  20086  uvcresum  20132  frlmup1  20137  frlmup2  20138  islinds  20148  islindf5  20178  mamulid  20247  mamurid  20248  mdetleib  20393  mdetleib1  20397  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  cpmidpmatlem1  20675  ordtval  20993  cnpval  21040  ptpjpre1  21374  ptpjopn  21415  dfac14  21421  upxp  21426  uptx  21428  hauseqlcld  21449  txlm  21451  xkoptsub  21457  xkoinjcn  21490  kqval  21529  xpstopnlem1  21612  fmval  21747  flfval  21794  ptcmplem2  21857  ptcmplem3  21858  symgtgp  21905  qustgpopn  21923  ussval  22063  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  mopnval  22243  prdsxmslem2  22334  nmfval  22393  nmval  22394  nmoval  22519  metdsval  22650  divcn  22671  mulc1cncf  22708  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  cnheiborlem  22753  evth  22758  evth2  22759  lebnumlem3  22762  isphtpy  22780  isphtpc  22793  pcofval  22810  pcovalg  22812  pco1  22815  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevcl  22825  pcorevlem  22826  pcorev2  22828  pi1xfrcnv  22857  cphnm  22993  tchval  23017  tchnmval  23028  cfilfval  23062  iscmet  23082  iscmet3lem3  23088  rrxval  23175  ehlval  23193  ivth2  23224  ovolval  23242  ovollb2lem  23256  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolicc1  23284  voliunlem1  23318  voliunlem2  23319  voliunlem3  23320  volsup  23324  ioorval  23342  uniioombllem3  23353  uniioombllem6  23356  volsup2  23373  volcn  23374  volivth  23375  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  vitali  23382  mbfmax  23416  mbfimaopnlem  23422  itg1val  23450  i1f1lem  23456  itg11  23458  itg1addlem4  23466  itg1mulc  23471  i1fres  23472  itg1climres  23481  mbfi1fseqlem2  23483  mbfi1fseqlem3  23484  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfi1flim  23490  mbfmullem2  23491  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  itg2cnlem1  23528  itg2cn  23530  limccnp2  23656  dvnff  23686  dvnp1  23688  cpnfval  23695  elcpn  23697  dvrec  23718  dvcnvlem  23739  dveflem  23742  dvef  23743  dvferm1  23748  dvferm2  23750  rolle  23753  dvlip  23756  dvlipcn  23757  dv11cn  23764  dvivthlem1  23771  dvivth  23773  lhop1lem  23776  ftc1lem1  23798  ftc1lem5  23803  ftc2  23807  itgsubstlem  23811  tdeglem3  23819  tdeglem4  23820  mdegval  23823  mdegmullem  23838  deg1fval  23840  deg1ldg  23852  deg1leb  23855  coe1mul3  23859  uc1pval  23899  mon1pval  23901  q1pval  23913  r1pval  23916  ply1remlem  23922  ig1pval  23932  plyval  23949  elply2  23952  plyeq0lem  23966  coeval  23979  dgrval  23984  coeid2  23995  coemullem  24006  coemul  24008  elqaalem1  24074  elqaalem2  24075  elqaalem3  24076  iaa  24080  aareccl  24081  aannenlem1  24083  geolim3  24094  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  aaliou3  24106  tayl0  24116  taylthlem1  24127  taylthlem2  24128  ulmshftlem  24143  ulmshft  24144  ulmuni  24146  ulmcau  24149  ulmdvlem1  24154  ulmdvlem3  24156  mtest  24158  mtestbdd  24159  mbfulm  24160  iblulm  24161  itgulm  24162  pserval  24164  pserval2  24165  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  pserulm  24176  pserdvlem2  24182  pserdv  24183  abelthlem1  24185  abelthlem3  24187  abelthlem4  24188  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  resinf1o  24282  efif1olem4  24291  eff1olem  24294  logcnlem5  24392  logtayllem  24405  logtayl  24406  logtaylsum  24407  logtayl2  24408  logccv  24409  asinval  24609  acosval  24610  atanval  24611  atantayl  24664  leibpilem2  24668  leibpi  24669  leibpisum  24670  log2cnv  24671  log2tlbnd  24672  areaval  24691  efrlim  24696  dfef2  24697  amgmlem  24716  emcllem2  24723  emcllem3  24724  emcllem4  24725  emcllem5  24726  emcllem6  24727  emcllem7  24728  zetacvg  24741  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulm2  24762  lgamcvglem  24766  igamval  24773  lgamcvg2  24781  gamcvg2lem  24785  ftalem7  24805  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  basellem6  24812  basellem8  24814  basellem9  24815  chtval  24836  vmaval  24839  chpval  24848  ppival  24853  muval  24858  prmorcht  24904  sqff1o  24908  dvdsflsumcom  24914  musum  24917  muinv  24919  sgmppw  24922  fsumvma  24938  pclogsum  24940  dchrfi  24980  bposlem5  25013  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgsfval  25027  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  lgsqrlem2  25072  lgsqrlem4  25074  lgseisenlem2  25101  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0fval  25194  dchrisum0re  25202  mulog2sumlem1  25223  pntrval  25251  pntsval  25261  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntlem3  25298  abvcxp  25304  padicfval  25305  padicval  25306  padicabv  25319  ostth1  25322  ostth2  25326  ostth3  25327  iscgrg  25407  legval  25479  ishlg  25497  ishpg  25651  iscgra  25701  isinag  25729  isleag  25733  iseqlg  25747  ttgval  25755  elee  25774  axsegconlem1  25797  axsegconlem9  25805  axsegconlem10  25806  axpasch  25821  axlowdimlem15  25836  axlowdim  25841  axeuclidlem  25842  axcontlem2  25845  eengv  25859  vtxval  25878  iedgval  25879  vtxvalOLD  25880  iedgvalOLD  25881  vtxdgval  26364  wlknwwlksninj  26775  wlknwwlksnsur  26776  wlkwwlkinj  26782  wlkwwlksur  26783  wwlksnextinj  26794  wwlksnextsur  26795  clwwlksfv  26916  fusgreg2wsplem  27197  fusgreghash2wsp  27202  numclwlk1lem2fv  27226  gidval  27366  grpoinvval  27377  bafval  27459  imsval  27540  dipfval  27557  sspval  27578  nmooval  27618  hmoval  27665  ipasslem8  27692  ipasslem9  27693  ipblnfi  27711  ubthlem2  27727  htthlem  27774  normval  27981  ocval  28139  occllem  28162  hsupval  28193  pjhfval  28255  pjhval  28256  chscllem2  28497  chscllem3  28498  hosval  28599  homval  28600  hodval  28601  hfsval  28602  hfmval  28603  brafval  28802  braval  28803  kbval  28813  eigvalval  28819  cnlnadjlem1  28926  nmopadjlei  28947  hmopidmchi  29010  strlem2  29110  hstrlem2  29118  cdj3lem2  29294  ofpreima  29465  inftmrel  29734  isinftm  29735  psgnfzto1stlem  29850  smatfval  29861  lmatval  29879  locfinreflem  29907  rmulccn  29974  xrmulc1cn  29976  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  xrge0iif1  29984  qqhval  30018  rrhval  30040  xrhval  30062  ddeval1  30297  ddeval0  30298  sxbrsigalem0  30333  sxbrsigalem3  30334  eulerpartlemgv  30435  rrvmbfm  30504  dstrvval  30532  coinflippv  30545  ballotlem2  30550  ballotlemfval  30551  ballotlemi  30562  ballotlemsval  30570  ballotlemrval  30579  ballotth  30599  plymulx  30625  signstfv  30640  signsvvfval  30655  derangval  31149  subfacval  31155  erdszelem3  31175  erdszelem9  31181  erdszelem10  31182  txpconn  31214  indispconn  31216  cvxpconn  31224  cvmlift2lem2  31286  cvmlift2lem3  31287  cvmlift2lem7  31291  cvmliftphtlem  31299  cvmlift3lem4  31304  snmlfval  31312  snmlval  31313  mvtval  31397  mvrsval  31402  mrsubffval  31404  mrsubcv  31407  mrsubrn  31410  elmrsubrn  31417  msubffval  31420  mvhfval  31430  mvhval  31431  mpstval  31432  msrfval  31434  mstaval  31441  mclsval  31460  mppsval  31469  sinccvglem  31566  circum  31568  divcnvlin  31618  iprodefisum  31627  iprodgam  31628  faclimlem1  31629  faclimlem2  31630  faclim  31632  iprodfac  31633  faclim2  31634  dfrdg2  31701  nosupfv  31852  findabrcl  32453  dnival  32461  bj-evalval  33027  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  curfv  33389  finixpnum  33394  poimirlem16  33425  poimir  33442  broucube  33443  mblfinlem2  33447  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  itg2addnclem3  33463  ftc1cnnc  33484  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493  ftc2nc  33494  fvopabf4g  33515  sdclem2  33538  fdc  33541  lmclim2  33554  geomcau  33555  istotbnd  33568  isbnd  33579  prdsbnd2  33594  heiborlem6  33615  heiborlem7  33616  heiborlem8  33617  rrnval  33626  rrncmslem  33631  idlval  33812  pridlval  33832  maxidlval  33838  lshpset  34265  lsatset  34277  lcvfbr  34307  lflset  34346  lflnegcl  34362  lkrfval  34374  lshpkrlem1  34397  lshpkrlem2  34398  lshpkrlem3  34399  ldualset  34412  cmtfvalN  34497  cvrfval  34555  pats  34572  llnset  34791  lplnset  34815  lvolset  34858  lineset  35024  pointsetN  35027  psubspset  35030  pmapfval  35042  pmapval  35043  paddfval  35083  pclfvalN  35175  polfvalN  35190  polvalN  35191  psubclsetN  35222  watfvalN  35278  watvalN  35279  lhpset  35281  lautset  35368  pautsetN  35384  ldilfset  35394  ldilset  35395  ltrnfset  35403  ltrnset  35404  dilfsetN  35439  dilsetN  35440  trnfsetN  35442  trnsetN  35443  trlfset  35447  trlset  35448  trlval  35449  tgrpfset  36032  tgrpset  36033  tendofset  36046  tendoset  36047  tendo02  36075  tendoi  36082  erngfset  36087  erngset  36088  erngfset-rN  36095  erngset-rN  36096  cdlemksv  36132  dvafset  36292  dvaset  36293  dvaplusgv  36298  diaffval  36319  diafval  36320  diaval  36321  dvhfset  36369  dvhset  36370  cdlemm10N  36407  docaffvalN  36410  docafvalN  36411  djaffvalN  36422  djafvalN  36423  dibffval  36429  dibfval  36430  dibval  36431  dicffval  36463  dicfval  36464  dicval  36465  dihffval  36519  dihfval  36520  dihval  36521  dochffval  36638  dochfval  36639  djhffval  36685  djhfval  36686  dochfl1  36765  lpolsetN  36771  lcfrlem8  36838  lcdfval  36877  lcdval  36878  mapdffval  36915  mapdfval  36916  mapdhval  37013  hvmapffval  37047  hvmapfval  37048  hdmap1ffval  37085  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapffval  37177  hgmapfval  37178  isnacs  37267  mzpclval  37288  mzpsubst  37311  mzprename  37312  mzpcompact2lem  37314  eldiophb  37320  diophrw  37322  eldioph2  37325  diophin  37336  diophun  37337  diophren  37377  pell1qrval  37410  pell14qrval  37412  pell1234qrval  37414  pellfundval  37444  rmxypairf1o  37476  rmxyval  37480  mzpcong  37539  pw2f1ocnv  37604  dnnumch1  37614  dfac11  37632  hbtlem1  37693  hbtlem7  37695  elmnc  37706  dgraaval  37714  mpaaval  37721  itgoval  37731  rgspnval  37738  flcidc  37744  mendval  37753  issdrg  37767  mon1pid  37783  cytpval  37787  elcnvlem  37907  comptiunov2i  37998  dftrcl3  38012  trclfvcom  38015  cnvtrclfv  38016  cotrcltrcl  38017  trclimalb2  38018  trclfvdecomr  38020  dfrtrcl3  38025  dfrtrcl4  38030  clsk1indlem0  38339  clsk1indlem2  38340  clsk1indlem3  38341  clsk1indlem4  38342  clsk1indlem1  38343  k0004val  38448  lhe4.4ex1a  38528  addrfv  38673  subrfv  38674  mulvfv  38675  sumnnodd  39862  liminfgval  39994  ioodvbdlimc2lem  40149  itgsin0pilem1  40165  stoweidlem55  40272  wallispilem1  40282  wallispilem2  40283  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  dirkerval  40308  fourierdlem2  40326  fourierdlem3  40327  fourierdlem29  40353  fourierdlem62  40385  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  fourierswlem  40447  fouriersw  40448  iundjiunlem  40676  carageniuncllem2  40736  0ome  40743  hoidmv1le  40808  hoidmvlelem3  40811  smflimsuplem7  41032  issubmgm  41789  vsetrec  42446  onsetreclem1  42448  elpglem3  42456  sinhval-named  42477  coshval-named  42478  tanhval-named  42479  secval  42488  cscval  42489  cotval  42490  aacllem  42547