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

Theorem fvmpt 5765
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 5763 . 2  |-  ( ( A  e.  D  /\  C  e.  _V )  ->  ( F `  A
)  =  C )
51, 4mpan2 653 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   _Vcvv 2916    e. cmpt 4226   ` cfv 5413
This theorem is referenced by:  fvmptex  5774  fvresex  5941  ofval  6273  caofinvl  6290  1stval  6310  2ndval  6311  reldm  6357  curry1val  6398  curry2val  6402  fnwelem  6420  brtpos2  6444  onovuni  6563  tz7.44-1  6623  oasuc  6727  oesuclem  6728  omsuc  6729  onasuc  6731  onmsuc  6732  fvmptmap  7009  xpcomco  7157  unxpdomlem1  7272  unfilem2  7331  ordtypelem3  7445  ixpiunwdom  7515  inf3lema  7535  noinfep  7570  cantnfval  7579  cantnflem1d  7600  cantnflem1  7601  r1sucg  7651  r0weon  7850  infxpenc2lem1  7856  fseqenlem1  7861  fseqenlem2  7862  dfac8alem  7866  ac5num  7873  acni2  7883  dfac4  7959  dfac2a  7966  dfacacn  7977  dfac12lem1  7979  ackbij1lem7  8062  ackbij2lem2  8076  ackbij2lem3  8077  cfsmolem  8106  fin23lem28  8176  fin23lem39  8186  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  fin1a2lem3  8238  itunifval  8252  itunisuc  8255  axdc2lem  8284  axdc3lem2  8287  axcclem  8293  zorn2lem1  8332  negiso  9940  infmsup  9942  uzval  10446  flval  11158  monoord2  11309  seqf1olem2  11318  seqf1o  11319  seqdistr  11329  serle  11333  seqof  11335  swrdfv  11726  revval  11747  revfv  11750  cjval  11862  reval  11866  imval  11867  sqrval  11997  absval  11998  limsupval  12223  limsupgval  12225  climmpt  12320  climle  12388  rlimdiv  12394  isercolllem1  12413  isercoll2  12417  caurcvg2  12426  fsumser  12479  isumadd  12506  fsumcnv  12512  fsumrev  12517  fsumshft  12518  iserabs  12549  cvgcmp  12550  cvgcmpce  12552  incexclem  12571  isumless  12580  supcvg  12590  harmonic  12593  trireciplem  12596  trirecip  12597  expcnv  12598  explecnv  12599  geolim  12602  geolim2  12603  geo2lim  12607  geomulcvg  12608  geoisum  12609  geoisumr  12610  geoisum1  12611  geoisum1c  12612  cvgrat  12615  mertenslem2  12617  mertens  12618  eftval  12634  efval  12637  efcvgfsum  12643  ege2le3  12647  eftlub  12665  eflegeo  12677  sinval  12678  cosval  12679  tanval  12684  eirrlem  12758  rpnnen2lem1  12769  rpnnen2lem2  12770  bitsfval  12890  bitsinv2  12910  bitsinv  12915  sadcf  12920  sadc0  12921  sadcp1  12922  smupf  12945  smup0  12946  smupp1  12947  qnumval  13084  qdenval  13085  phival  13111  crt  13122  phimullem  13123  eulerthlem2  13126  odzval  13132  iserodd  13164  pcmpt  13216  prmreclem1  13239  prmreclem2  13240  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  1arithlem1  13246  1arithlem2  13247  vdwapfval  13294  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  ramub1lem2  13350  ramcl  13352  strfvnd  13439  topnval  13617  prdsplusgfval  13651  prdsmulrfval  13653  isacs  13831  acsfn  13839  cidfval  13856  homffval  13872  comfffval  13879  oppcval  13894  monfval  13913  oppcmon  13919  sectffval  13931  invffval  13938  isoval  13945  idfuval  14028  homafval  14139  arwval  14153  idafval  14167  coafval  14174  yonedainv  14333  pltfval  14371  lubfval  14390  lubval  14391  glbfval  14395  glbval  14396  joinfval  14399  meetfval  14406  p0val  14425  p1val  14426  oduval  14512  ipoval  14535  plusffval  14657  grpidval  14662  issubm  14703  prdspjmhm  14721  grpinvfval  14798  grpinvval  14799  grpsubfval  14802  grplactfval  14840  grplactval  14841  mulgfval  14846  prdsinvlem  14881  pwsmulg  14887  issubg  14899  cycsubgcl  14921  isnsg  14924  conjghm  14991  conjnmz  14994  symgval  15049  cntrval  15073  cntzfval  15074  cntzval  15075  oppgval  15098  odfval  15126  odval  15127  sylow1lem4  15190  pgpssslw  15203  sylow2blem3  15211  sylow3lem2  15217  lsmfval  15227  pj1fval  15281  efgval  15304  efgsval  15318  frgpval  15345  vrgpval  15354  mulgmhm  15405  mulgghm  15406  ablfaclem1  15598  mgpval  15606  rnglghm  15666  rngrghm  15667  opprval  15684  dvdsrval  15705  isunit  15717  invrfval  15733  dvrfval  15744  isirred  15759  issubrg  15823  abvfval  15861  abvtrivd  15883  staffval  15890  stafval  15891  scaffval  15923  lmodvsghm  15960  lssset  15965  lspfval  16004  islbs  16103  sraval  16203  rlmval  16219  2idlval  16259  lpival  16271  rrgval  16302  fidomndrnglem  16321  aspval  16342  asclfval  16348  asclval  16349  psrmulval  16405  psrlidm  16422  psrridm  16423  mvrval  16440  mvrval2  16441  mplmonmul  16482  psr1val  16539  vr1val  16545  ply1val  16547  coe1fval  16558  coe1fv  16559  coe1tmmul2  16623  coe1tmmul  16624  coe1tmmul2fv  16625  coe1pwmulfv  16627  expmhm  16731  expghm  16732  mulgghm2  16741  mulgrhm  16742  zrhval  16744  zrhmulg  16746  zlmval  16752  chrval  16761  znval  16771  znzrhval  16782  ip0l  16822  ipffval  16834  ocvfval  16848  ocvval  16849  cssval  16864  thlval  16877  pjfval  16888  pjval  16892  isobs  16902  ordtval  17207  cnpval  17254  ptpjpre1  17556  ptpjopn  17597  dfac14  17603  upxp  17608  uptx  17610  hauseqlcld  17631  txlm  17633  xkoptsub  17639  xkoinjcn  17672  kqval  17711  xpstopnlem1  17794  fmval  17928  flfval  17975  ptcmplem2  18037  ptcmplem3  18038  symgtgp  18084  divstgpopn  18102  ussval  18242  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  mopnval  18421  prdsxmslem2  18512  nmfval  18589  nmval  18590  nmoval  18702  metdsval  18830  divcn  18851  mulc1cncf  18888  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  cnheiborlem  18932  evth  18937  evth2  18938  lebnumlem3  18941  isphtpy  18959  isphtpc  18972  pcofval  18988  pcovalg  18990  pco1  18993  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevcl  19003  pcorevlem  19004  pcorev2  19006  pi1xfrcnv  19035  cphnm  19109  tchval  19130  tchnmval  19140  cfilfval  19170  iscmet  19190  iscmet3lem3  19196  ivth2  19305  ovolval  19323  ovollb2lem  19337  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovolicc1  19365  voliunlem1  19397  voliunlem2  19398  voliunlem3  19399  volsup  19403  ioorval  19419  uniioombllem3  19430  uniioombllem6  19433  volsup2  19450  volcn  19451  volivth  19452  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  vitali  19458  mbfmax  19494  mbfimaopnlem  19500  itg1val  19528  i1f1lem  19534  itg11  19536  itg1addlem4  19544  itg1mulc  19549  i1fres  19550  itg1climres  19559  mbfi1fseqlem2  19561  mbfi1fseqlem3  19562  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfi1flim  19568  mbfmullem2  19569  itg2seq  19587  itg2uba  19588  itg2splitlem  19593  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  itg2cnlem1  19606  itg2cn  19608  limccnp2  19732  dvnff  19762  dvnp1  19764  cpnfval  19771  elcpn  19773  dvrec  19794  dvcnvlem  19813  dveflem  19816  dvef  19817  dvferm1  19822  dvferm2  19824  rolle  19827  dvlip  19830  dvlipcn  19831  dv11cn  19838  dvivthlem1  19845  dvivth  19847  lhop1lem  19850  ftc1lem1  19872  ftc1lem5  19877  ftc2  19881  itgsubstlem  19885  evlslem3  19888  evlslem1  19889  evlsval  19893  evlssca  19896  evlsvar  19897  evl1fval  19900  evl1val  19901  tdeglem3  19935  tdeglem4  19936  mdegval  19939  mdegmullem  19954  deg1fval  19956  deg1ldg  19968  deg1leb  19971  coe1mul3  19975  uc1pval  20015  mon1pval  20017  q1pval  20029  r1pval  20032  ply1remlem  20038  ig1pval  20048  plyval  20065  elply2  20068  plyeq0lem  20082  coeval  20095  dgrval  20100  coeid2  20111  coemullem  20121  coemul  20123  elqaalem1  20189  elqaalem2  20190  elqaalem3  20191  iaa  20195  aareccl  20196  aannenlem1  20198  geolim3  20209  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem5  20217  aaliou3lem6  20218  aaliou3lem7  20219  aaliou3  20221  tayl0  20231  taylthlem1  20242  taylthlem2  20243  ulmshftlem  20258  ulmshft  20259  ulmuni  20261  ulmcau  20264  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  mtestbdd  20274  mbfulm  20275  iblulm  20276  itgulm  20277  pserval  20279  pserval2  20280  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  pserulm  20291  pserdvlem2  20297  pserdv  20298  abelthlem1  20300  abelthlem3  20302  abelthlem4  20303  abelthlem5  20304  abelthlem6  20305  abelthlem7  20307  abelthlem8  20308  abelthlem9  20309  resinf1o  20391  efgh  20396  efif1olem4  20400  eff1olem  20403  logcnlem5  20490  logtayllem  20503  logtayl  20504  logtaylsum  20505  logtayl2  20506  logccv  20507  asinval  20675  acosval  20676  atanval  20677  atantayl  20730  leibpilem2  20734  leibpi  20735  leibpisum  20736  log2cnv  20737  log2tlbnd  20738  areaval  20756  efrlim  20761  dfef2  20762  amgmlem  20781  emcllem2  20788  emcllem3  20789  emcllem4  20790  emcllem5  20791  emcllem6  20792  emcllem7  20793  ftalem7  20814  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  basellem6  20821  basellem8  20823  basellem9  20824  chtval  20846  vmaval  20849  chpval  20858  ppival  20863  muval  20868  prmorcht  20914  sqff1o  20918  dvdsflsumcom  20926  musum  20929  muinv  20931  sgmppw  20934  fsumvma  20950  pclogsum  20952  dchrfi  20992  bposlem5  21025  bposlem7  21027  bposlem8  21028  bposlem9  21029  lgsfval  21038  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgsqrlem2  21079  lgsqrlem4  21081  lgseisenlem2  21087  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasumiflem1  21148  dchrvmaeq0  21151  dchrisum0fval  21152  dchrisum0re  21160  mulog2sumlem1  21181  pntrval  21209  pntsval  21219  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntlem3  21256  abvcxp  21262  padicfval  21263  padicval  21264  padicabv  21277  ostth1  21280  ostth2  21284  ostth3  21285  vdgrval  21620  gidval  21754  grpoinvval  21766  bafval  22036  imsval  22130  dipfval  22151  sspval  22175  nmooval  22217  hmoval  22264  ipasslem8  22291  ipasslem9  22292  ipblnfi  22310  ubthlem2  22326  htthlem  22373  normval  22579  ocval  22735  occllem  22758  hsupval  22789  pjhfval  22851  pjhval  22852  chscllem2  23093  chscllem3  23094  hosval  23196  homval  23197  hodval  23198  hfsval  23199  hfmval  23200  brafval  23399  braval  23400  kbval  23410  eigvalval  23416  cnlnadjlem1  23523  nmopadjlei  23544  hmopidmchi  23607  strlem2  23707  hstrlem2  23715  cdj3lem2  23891  ofpreima  24034  inftmrel  24203  isinftm  24204  rmulccn  24267  xrmulc1cn  24269  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhom  24276  xrge0iif1  24277  qqhval  24311  rrhval  24332  xrhval  24337  sxbrsigalem0  24574  sxbrsigalem3  24575  rrvmbfm  24653  dstrvval  24681  coinflippv  24694  ballotlem2  24699  ballotlemfval  24700  ballotlemi  24711  ballotlemsval  24719  ballotlemrval  24728  ballotth  24748  zetacvg  24752  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulm2  24773  lgamcvglem  24777  igamval  24784  lgamcvg2  24792  gamcvg2lem  24796  derangval  24806  subfacval  24812  erdszelem3  24832  erdszelem9  24838  erdszelem10  24839  txpcon  24872  indispcon  24874  cvxpcon  24882  cvmlift2lem2  24944  cvmlift2lem3  24945  cvmlift2lem7  24949  cvmliftphtlem  24957  cvmlift3lem4  24962  snmlfval  24970  snmlval  24971  sinccvglem  25062  circum  25064  divcnvshft  25164  divcnvlin  25165  prodfdiv  25177  fprodser  25228  fprodshft  25253  fprodrev  25254  fprodcnv  25260  iprodmul  25269  iprodefisum  25271  iprodgam  25272  faclimlem1  25310  faclimlem2  25311  faclim  25313  iprodfac  25314  faclim2  25315  dfrdg2  25366  elee  25737  axsegconlem1  25760  axsegconlem9  25768  axsegconlem10  25769  axpasch  25784  axlowdimlem15  25799  axlowdim  25804  axeuclidlem  25805  axcontlem2  25808  bpolylem  25998  findabrcl  26108  mblfinlem  26143  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  itg2addnclem3  26157  ftc1cnnc  26178  fvopabf4g  26312  sdclem2  26336  fdc  26339  lmclim2  26354  geomcau  26355  istotbnd  26368  isbnd  26379  prdsbnd2  26394  heiborlem6  26415  heiborlem7  26416  heiborlem8  26417  rrnval  26426  rrncmslem  26431  idlval  26513  pridlval  26533  maxidlval  26539  isnacs  26648  mzpclval  26672  mzpsubst  26695  mzprename  26696  mzpcompact2lem  26698  eldiophb  26705  diophrw  26707  eldioph2  26710  diophin  26721  diophun  26722  diophren  26764  pell1qrval  26799  pell14qrval  26801  pell1234qrval  26803  pellfundval  26833  rmxypairf1o  26864  rmxyval  26868  mzpcong  26927  pw2f1ocnv  26998  dnnumch1  27009  dfac11  27028  prdsinvgd2  27076  uvcresum  27110  frlmup1  27118  frlmup2  27119  islinds  27147  islindf5  27177  hbtlem1  27195  hbtlem7  27197  elmnc  27209  dgraaval  27217  mpaaval  27224  itgoval  27234  rgspnval  27241  flcidc  27247  psgnfval  27291  psgnval  27298  mamulid  27326  mamurid  27327  mdetleib  27356  mendval  27359  issdrg  27373  phisum  27386  mon1pid  27392  cytpval  27396  lhe4.4ex1a  27414  addrfv  27541  subrfv  27542  mulvfv  27543  itgsin0pilem1  27611  stoweidlem55  27671  wallispilem1  27681  wallispilem2  27682  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  sinhval-named  28193  coshval-named  28194  tanhval-named  28195  secval  28204  cscval  28205  cotval  28206  sgnval  28232  ceilingval  28242  lshpset  29461  lsatset  29473  lcvfbr  29503  lflset  29542  lflnegcl  29558  lkrfval  29570  lshpkrlem1  29593  lshpkrlem2  29594  lshpkrlem3  29595  ldualset  29608  cmtfvalN  29693  cvrfval  29751  pats  29768  llnset  29987  lplnset  30011  lvolset  30054  lineset  30220  pointsetN  30223  psubspset  30226  pmapfval  30238  pmapval  30239  paddfval  30279  pclfvalN  30371  polfvalN  30386  polvalN  30387  psubclsetN  30418  watfvalN  30474  watvalN  30475  lhpset  30477  lautset  30564  pautsetN  30580  ldilfset  30590  ldilset  30591  ltrnfset  30599  ltrnset  30600  dilfsetN  30634  dilsetN  30635  trnfsetN  30637  trnsetN  30638  trlfset  30642  trlset  30643  trlval  30644  tgrpfset  31226  tgrpset  31227  tendofset  31240  tendoset  31241  tendo02  31269  tendoi  31276  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  cdlemksv  31326  dvafset  31486  dvaset  31487  dvaplusgv  31492  diaffval  31513  diafval  31514  diaval  31515  dvhfset  31563  dvhset  31564  cdlemm10N  31601  docaffvalN  31604  docafvalN  31605  djaffvalN  31616  djafvalN  31617  dibffval  31623  dibfval  31624  dibval  31625  dicffval  31657  dicfval  31658  dicval  31659  dihffval  31713  dihfval  31714  dihval  31715  dochffval  31832  dochfval  31833  djhffval  31879  djhfval  31880  dochfl1  31959  lpolsetN  31965  lcfrlem8  32032  lcdfval  32071  lcdval  32072  mapdffval  32109  mapdfval  32110  mapdhval  32207  hvmapffval  32241  hvmapfval  32242  hdmap1ffval  32279  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421
  Copyright terms: Public domain W3C validator