MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpt Unicode version

Theorem fvmpt 5604
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
StepHypRef 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 )
42, 3fvmptg 5602 . 2  |-  ( ( A  e.  D  /\  C  e.  _V )  ->  ( F `  A
)  =  C )
51, 4mpan2 652 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. wcel 1686   _Vcvv 2790    e. cmpt 4079   ` cfv 5257
This theorem is referenced by:  fvmptex  5612  fvresex  5764  ofval  6089  caofinvl  6106  1stval  6126  2ndval  6127  reldm  6173  curry1val  6213  curry2val  6217  fnwelem  6232  brtpos2  6242  onovuni  6361  tz7.44-1  6421  oasuc  6525  oesuclem  6526  omsuc  6527  onasuc  6529  onmsuc  6530  fvmptmap  6806  xpcomco  6954  unxpdomlem1  7069  unfilem2  7124  ordtypelem3  7237  ixpiunwdom  7307  inf3lema  7327  noinfep  7362  cantnfval  7371  cantnflem1d  7392  cantnflem1  7393  r1sucg  7443  r0weon  7642  infxpenc2lem1  7648  fseqenlem1  7653  fseqenlem2  7654  dfac8alem  7658  ac5num  7665  acni2  7675  dfac4  7751  dfac2a  7758  dfacacn  7769  dfac12lem1  7771  ackbij1lem7  7854  ackbij2lem2  7868  ackbij2lem3  7869  cfsmolem  7898  fin23lem28  7968  fin23lem39  7978  isf32lem6  7986  isf32lem7  7987  isf32lem8  7988  fin1a2lem3  8030  itunifval  8044  itunisuc  8047  axdc2lem  8076  axdc3lem2  8079  axcclem  8085  zorn2lem1  8125  negiso  9732  infmsup  9734  uzval  10234  flval  10928  monoord2  11079  seqf1olem2  11088  seqf1o  11089  seqdistr  11099  serle  11103  seqof  11105  swrdfv  11459  revval  11480  revfv  11483  cjval  11589  reval  11593  imval  11594  sqrval  11724  absval  11725  limsupval  11950  limsupgval  11952  climmpt  12047  climle  12115  rlimdiv  12121  isercolllem1  12140  isercoll2  12144  caurcvg2  12152  fsumser  12205  isumadd  12232  fsumcnv  12238  fsumrev  12243  fsumshft  12244  iserabs  12275  cvgcmp  12276  cvgcmpce  12278  incexclem  12297  isumless  12306  supcvg  12316  harmonic  12319  trireciplem  12322  trirecip  12323  expcnv  12324  explecnv  12325  geolim  12328  geolim2  12329  geo2lim  12333  geomulcvg  12334  geoisum  12335  geoisumr  12336  geoisum1  12337  geoisum1c  12338  cvgrat  12341  mertenslem2  12343  mertens  12344  eftval  12360  efval  12363  efcvgfsum  12369  ege2le3  12373  eftlub  12391  eflegeo  12403  sinval  12404  cosval  12405  tanval  12410  eirrlem  12484  rpnnen2lem1  12495  rpnnen2lem2  12496  bitsfval  12616  bitsinv2  12636  bitsinv  12641  sadcf  12646  sadc0  12647  sadcp1  12648  smupf  12671  smup0  12672  smupp1  12673  qnumval  12810  qdenval  12811  phival  12837  crt  12848  phimullem  12849  eulerthlem2  12852  odzval  12858  iserodd  12890  pcmpt  12942  prmreclem1  12965  prmreclem2  12966  prmreclem4  12968  prmreclem5  12969  prmreclem6  12970  1arithlem1  12972  1arithlem2  12973  vdwapfval  13020  vdwlem2  13031  vdwlem6  13035  vdwlem8  13037  vdwlem9  13038  ramub1lem2  13076  ramcl  13078  strfvnd  13165  topnval  13341  prdsplusgfval  13375  prdsmulrfval  13377  isacs  13555  acsfn  13563  cidfval  13580  homffval  13596  comfffval  13603  oppcval  13618  monfval  13637  oppcmon  13643  sectffval  13655  invffval  13662  isoval  13669  idfuval  13752  homafval  13863  arwval  13877  idafval  13891  coafval  13898  yonedainv  14057  pltfval  14095  lubfval  14114  lubval  14115  glbfval  14119  glbval  14120  joinfval  14123  meetfval  14130  p0val  14149  p1val  14150  oduval  14236  ipoval  14259  plusffval  14381  grpidval  14386  issubm  14427  prdspjmhm  14445  grpinvfval  14522  grpinvval  14523  grpsubfval  14526  grplactfval  14564  grplactval  14565  mulgfval  14570  prdsinvlem  14605  pwsmulg  14611  issubg  14623  cycsubgcl  14645  isnsg  14648  conjghm  14715  conjnmz  14718  symgval  14773  cntrval  14797  cntzfval  14798  cntzval  14799  oppgval  14822  odfval  14850  odval  14851  sylow1lem4  14914  pgpssslw  14927  sylow2blem3  14935  sylow3lem2  14941  lsmfval  14951  pj1fval  15005  efgval  15028  efgsval  15042  frgpval  15069  vrgpval  15078  mulgmhm  15129  mulgghm  15130  ablfaclem1  15322  mgpval  15330  rnglghm  15390  rngrghm  15391  opprval  15408  dvdsrval  15429  isunit  15441  invrfval  15457  dvrfval  15468  isirred  15483  issubrg  15547  abvfval  15585  abvtrivd  15607  staffval  15614  stafval  15615  scaffval  15647  lmodvsghm  15688  lssset  15693  lspfval  15732  islbs  15831  sraval  15931  rlmval  15947  2idlval  15987  lpival  15999  rrgval  16030  fidomndrnglem  16049  aspval  16070  asclfval  16076  asclval  16077  psrmulval  16133  psrlidm  16150  psrridm  16151  mvrval  16168  mvrval2  16169  mplmonmul  16210  psr1val  16267  vr1val  16273  ply1val  16275  coe1fval  16288  coe1fv  16289  coe1tmmul2  16354  coe1tmmul  16355  coe1tmmul2fv  16356  coe1pwmulfv  16358  expmhm  16451  expghm  16452  mulgghm2  16461  mulgrhm  16462  zrhval  16464  zrhmulg  16466  zlmval  16472  chrval  16481  znval  16491  znzrhval  16502  ip0l  16542  ipffval  16554  ocvfval  16568  ocvval  16569  cssval  16584  thlval  16597  pjfval  16608  pjval  16612  isobs  16622  ordtval  16921  cnpval  16968  ptpjpre1  17268  ptpjopn  17308  dfac14  17314  upxp  17319  uptx  17321  hauseqlcld  17342  txlm  17344  xkoptsub  17350  xkoinjcn  17383  kqval  17419  xpstopnlem1  17502  fmval  17640  flfval  17687  ptcmplem2  17749  ptcmplem3  17750  symgtgp  17786  divstgpopn  17804  ismet  17890  isxmet  17891  mopnval  17986  prdsxmslem2  18077  nmfval  18113  nmval  18114  nmoval  18226  metdsval  18353  divcn  18374  mulc1cncf  18411  icopnfhmeo  18443  iccpnfhmeo  18445  xrhmeo  18446  cnheiborlem  18454  evth  18459  evth2  18460  lebnumlem3  18463  isphtpy  18481  isphtpc  18494  pcofval  18510  pcovalg  18512  pco1  18515  pcopt  18522  pcopt2  18523  pcoass  18524  pcorevcl  18525  pcorevlem  18526  pcorev2  18528  pi1xfrcnv  18557  cphnm  18631  tchval  18652  tchnmval  18662  cfilfval  18692  iscmet  18712  iscmet3lem3  18718  ivth2  18817  ovolval  18835  ovollb2lem  18849  ovolunlem1a  18857  ovolunlem1  18858  ovoliunlem1  18863  ovoliunlem2  18864  ovolicc1  18877  voliunlem1  18909  voliunlem2  18910  voliunlem3  18911  volsup  18915  ioorval  18931  uniioombllem3  18942  uniioombllem6  18945  volsup2  18962  volcn  18963  volivth  18964  vitalilem2  18966  vitalilem3  18967  vitalilem4  18968  vitali  18970  mbfmax  19006  mbfimaopnlem  19012  itg1val  19040  i1f1lem  19046  itg11  19048  itg1addlem4  19056  itg1mulc  19061  i1fres  19062  itg1climres  19071  mbfi1fseqlem2  19073  mbfi1fseqlem3  19074  mbfi1fseqlem6  19077  mbfi1flimlem  19079  mbfi1flim  19080  mbfmullem2  19081  itg2seq  19099  itg2uba  19100  itg2splitlem  19105  itg2monolem1  19107  itg2monolem2  19108  itg2monolem3  19109  itg2mono  19110  itg2i1fseqle  19111  itg2i1fseq  19112  itg2i1fseq2  19113  itg2addlem  19115  itg2cnlem1  19118  itg2cn  19120  limccnp2  19244  dvnff  19274  dvnp1  19276  cpnfval  19283  elcpn  19285  dvrec  19306  dvcnvlem  19325  dveflem  19328  dvef  19329  dvferm1  19334  dvferm2  19336  rolle  19339  dvlip  19342  dvlipcn  19343  dv11cn  19350  dvivthlem1  19357  dvivth  19359  lhop1lem  19362  ftc1lem1  19384  ftc1lem5  19389  ftc2  19393  itgsubstlem  19397  evlslem3  19400  evlslem1  19401  evlsval  19405  evlssca  19408  evlsvar  19409  evl1fval  19412  evl1val  19413  tdeglem3  19447  tdeglem4  19448  mdegval  19451  mdegmullem  19466  deg1fval  19468  deg1ldg  19480  deg1leb  19483  coe1mul3  19487  uc1pval  19527  mon1pval  19529  q1pval  19541  r1pval  19544  ply1remlem  19550  ig1pval  19560  plyval  19577  elply2  19580  plyeq0lem  19594  coeval  19607  dgrval  19612  coeid2  19623  coemullem  19633  coemul  19635  elqaalem1  19701  elqaalem2  19702  elqaalem3  19703  iaa  19707  aareccl  19708  aannenlem1  19710  geolim3  19721  aaliou3lem1  19724  aaliou3lem2  19725  aaliou3lem5  19729  aaliou3lem6  19730  aaliou3lem7  19731  aaliou3  19733  tayl0  19743  taylthlem1  19754  taylthlem2  19755  ulmshftlem  19770  ulmshft  19771  ulmcau  19774  ulmdvlem1  19779  ulmdvlem3  19781  mtest  19783  mbfulm  19784  iblulm  19785  itgulm  19786  pserval  19788  pserval2  19789  radcnvlem1  19791  radcnvlem2  19792  dvradcnv  19799  pserulm  19800  pserdvlem2  19806  pserdv  19807  abelthlem1  19809  abelthlem3  19811  abelthlem4  19812  abelthlem5  19813  abelthlem6  19814  abelthlem7  19816  abelthlem8  19817  abelthlem9  19818  resinf1o  19900  efgh  19905  efif1olem4  19909  eff1olem  19912  logcnlem5  19995  logtayllem  20008  logtayl  20009  logtaylsum  20010  logtayl2  20011  logccv  20012  asinval  20180  acosval  20181  atanval  20182  atantayl  20235  leibpilem2  20239  leibpi  20240  leibpisum  20241  log2cnv  20242  log2tlbnd  20243  areaval  20261  efrlim  20266  dfef2  20267  amgmlem  20286  emcllem2  20292  emcllem3  20293  emcllem4  20294  emcllem5  20295  emcllem6  20296  emcllem7  20297  ftalem7  20318  basellem2  20321  basellem3  20322  basellem4  20323  basellem5  20324  basellem6  20325  basellem8  20327  basellem9  20328  chtval  20350  vmaval  20353  chpval  20362  ppival  20367  muval  20372  prmorcht  20418  sqff1o  20422  dvdsflsumcom  20430  musum  20433  muinv  20435  sgmppw  20438  fsumvma  20454  pclogsum  20456  dchrfi  20496  bposlem5  20529  bposlem7  20531  bposlem8  20532  bposlem9  20533  lgsfval  20542  lgsdir  20571  lgsdilem2  20572  lgsdi  20573  lgsne0  20574  lgsqrlem2  20583  lgsqrlem4  20585  lgseisenlem2  20591  dchrmusum2  20645  dchrvmasumlem1  20646  dchrvmasumiflem1  20652  dchrvmaeq0  20655  dchrisum0fval  20656  dchrisum0re  20664  mulog2sumlem1  20685  pntrval  20713  pntsval  20723  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntlem3  20760  abvcxp  20766  padicfval  20767  padicval  20768  padicabv  20781  ostth1  20784  ostth2  20788  ostth3  20789  gidval  20882  grpoinvval  20894  bafval  21162  imsval  21256  dipfval  21277  sspval  21301  nmooval  21343  hmoval  21390  ipasslem8  21417  ipasslem9  21418  ipblnfi  21436  ubthlem2  21452  htthlem  21499  normval  21705  ocval  21861  occllem  21884  hsupval  21915  pjhfval  21977  pjhval  21978  chscllem2  22219  chscllem3  22220  hosval  22322  homval  22323  hodval  22324  hfsval  22325  hfmval  22326  brafval  22525  braval  22526  kbval  22536  eigvalval  22542  cnlnadjlem1  22649  nmopadjlei  22670  hmopidmchi  22733  strlem2  22833  hstrlem2  22841  cdj3lem2  23017  ballotlem2  23049  ballotlemfval  23050  ballotlemi  23061  ballotlemsval  23069  ballotlemrval  23078  ballotth  23098  rmulccn  23303  xrmulc1cn  23305  xrge0iifcv  23318  xrge0iifiso  23319  xrge0iifhom  23321  xrge0iif1  23322  dya2iocrrnval  23584  rrvmbfm  23647  dstrvval  23673  coinflippv  23686  zetacvg  23691  dmgmseqn0  23698  derangval  23700  subfacval  23706  erdszelem3  23726  erdszelem9  23732  erdszelem10  23733  txpcon  23765  indispcon  23767  cvxpcon  23775  cvmlift2lem2  23837  cvmlift2lem3  23838  cvmlift2lem7  23842  cvmliftphtlem  23850  cvmlift3lem4  23855  vdgrval  23892  snmlfval  23915  snmlval  23916  sinccvglem  24007  circum  24009  dfrdg2  24154  elee  24524  axsegconlem1  24547  axsegconlem9  24555  axsegconlem10  24556  axpasch  24571  axlowdimlem15  24586  axlowdim  24591  axeuclidlem  24592  axcontlem2  24595  bpolylem  24785  findabrcl  24895  itg2addnclem  24933  itg2addnc  24935  valpr  25169  prjmapcp2  25181  valvalcurfn  25217  gepsup  25261  seinf  25262  fprodser  25331  fincmpzer  25361  rltrooo  25426  idlvalNEW  25456  cntrset  25613  isaddrv  25657  issubcv  25681  ishoma  25798  ismona  25820  isepia  25830  isiso  25836  cinvlem1  25839  cinvlem2  25840  issubcat  25856  vtarsu  25897  trclval  25905  domcatfun  25936  codcatfun  25945  isrocatset  25968  iscatset  25989  isconcl1b  26108  fvopabf4g  26397  sdclem2  26463  fdc  26466  lmclim2  26485  geomcau  26486  istotbnd  26504  isbnd  26515  prdsbnd2  26530  heiborlem6  26551  heiborlem7  26552  heiborlem8  26553  rrnval  26562  rrncmslem  26567  idlval  26649  pridlval  26669  maxidlval  26675  isnacs  26790  mzpclval  26814  mzpsubst  26837  mzprename  26838  mzpcompact2lem  26840  eldiophb  26847  diophrw  26849  eldioph2  26852  diophin  26863  diophun  26864  diophren  26907  pell1qrval  26942  pell14qrval  26944  pell1234qrval  26946  pellfundval  26976  rmxypairf1o  27007  rmxyval  27011  mzpcong  27070  pw2f1ocnv  27141  dnnumch1  27152  dfac11  27171  prdsinvgd2  27219  uvcresum  27253  frlmup1  27261  frlmup2  27262  islinds  27290  islindf5  27320  hbtlem1  27338  hbtlem7  27340  elmnc  27352  dgraaval  27360  mpaaval  27367  itgoval  27377  rgspnval  27384  flcidc  27390  psgnfval  27434  psgnval  27441  mamulid  27469  mamurid  27470  mdetleib  27499  mendval  27502  issdrg  27516  phisum  27529  mon1pid  27535  cytpval  27539  lhe4.4ex1a  27557  addrfv  27685  subrfv  27686  mulvfv  27687  itgsin0pilem1  27755  stoweidlem55  27815  wallispilem1  27825  wallispilem2  27826  wallispilem4  27828  wallispi2lem1  27831  wallispi2lem2  27832  sinhval-named  28217  coshval-named  28218  tanhval-named  28219  secval  28228  cscval  28229  cotval  28230  sgnval  28256  ceilingval  28266  lshpset  29241  lsatset  29253  lcvfbr  29283  lflset  29322  lflnegcl  29338  lkrfval  29350  lshpkrlem1  29373  lshpkrlem2  29374  lshpkrlem3  29375  ldualset  29388  cmtfvalN  29473  cvrfval  29531  pats  29548  llnset  29767  lplnset  29791  lvolset  29834  lineset  30000  pointsetN  30003  psubspset  30006  pmapfval  30018  pmapval  30019  paddfval  30059  pclfvalN  30151  polfvalN  30166  polvalN  30167  psubclsetN  30198  watfvalN  30254  watvalN  30255  lhpset  30257  lautset  30344  pautsetN  30360  ldilfset  30370  ldilset  30371  ltrnfset  30379  ltrnset  30380  dilfsetN  30414  dilsetN  30415  trnfsetN  30417  trnsetN  30418  trlfset  30422  trlset  30423  trlval  30424  tgrpfset  31006  tgrpset  31007  tendofset  31020  tendoset  31021  tendo02  31049  tendoi  31056  erngfset  31061  erngset  31062  erngfset-rN  31069  erngset-rN  31070  cdlemksv  31106  dvafset  31266  dvaset  31267  dvaplusgv  31272  diaffval  31293  diafval  31294  diaval  31295  dvhfset  31343  dvhset  31344  cdlemm10N  31381  docaffvalN  31384  docafvalN  31385  djaffvalN  31396  djafvalN  31397  dibffval  31403  dibfval  31404  dibval  31405  dicffval  31437  dicfval  31438  dicval  31439  dihffval  31493  dihfval  31494  dihval  31495  dochffval  31612  dochfval  31613  djhffval  31659  djhfval  31660  dochfl1  31739  lpolsetN  31745  lcfrlem8  31812  lcdfval  31851  lcdval  31852  mapdffval  31889  mapdfval  31890  mapdhval  31987  hvmapffval  32021  hvmapfval  32022  hdmap1ffval  32059  hdmap1fval  32060  hdmapffval  32092  hdmapfval  32093  hgmapffval  32151  hgmapfval  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-iota 5221  df-fun 5259  df-fv 5265
  Copyright terms: Public domain W3C validator