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

Theorem fvmpt 5747
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 5745 . 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 1717   _Vcvv 2901    e. cmpt 4209   ` cfv 5396
This theorem is referenced by:  fvmptex  5756  fvresex  5923  ofval  6255  caofinvl  6272  1stval  6292  2ndval  6293  reldm  6339  curry1val  6380  curry2val  6384  fnwelem  6399  brtpos2  6423  onovuni  6542  tz7.44-1  6602  oasuc  6706  oesuclem  6707  omsuc  6708  onasuc  6710  onmsuc  6711  fvmptmap  6988  xpcomco  7136  unxpdomlem1  7251  unfilem2  7310  ordtypelem3  7424  ixpiunwdom  7494  inf3lema  7514  noinfep  7549  cantnfval  7558  cantnflem1d  7579  cantnflem1  7580  r1sucg  7630  r0weon  7829  infxpenc2lem1  7835  fseqenlem1  7840  fseqenlem2  7841  dfac8alem  7845  ac5num  7852  acni2  7862  dfac4  7938  dfac2a  7945  dfacacn  7956  dfac12lem1  7958  ackbij1lem7  8041  ackbij2lem2  8055  ackbij2lem3  8056  cfsmolem  8085  fin23lem28  8155  fin23lem39  8165  isf32lem6  8173  isf32lem7  8174  isf32lem8  8175  fin1a2lem3  8217  itunifval  8231  itunisuc  8234  axdc2lem  8263  axdc3lem2  8266  axcclem  8272  zorn2lem1  8311  negiso  9918  infmsup  9920  uzval  10424  flval  11132  monoord2  11283  seqf1olem2  11292  seqf1o  11293  seqdistr  11303  serle  11307  seqof  11309  swrdfv  11700  revval  11721  revfv  11724  cjval  11836  reval  11840  imval  11841  sqrval  11971  absval  11972  limsupval  12197  limsupgval  12199  climmpt  12294  climle  12362  rlimdiv  12368  isercolllem1  12387  isercoll2  12391  caurcvg2  12400  fsumser  12453  isumadd  12480  fsumcnv  12486  fsumrev  12491  fsumshft  12492  iserabs  12523  cvgcmp  12524  cvgcmpce  12526  incexclem  12545  isumless  12554  supcvg  12564  harmonic  12567  trireciplem  12570  trirecip  12571  expcnv  12572  explecnv  12573  geolim  12576  geolim2  12577  geo2lim  12581  geomulcvg  12582  geoisum  12583  geoisumr  12584  geoisum1  12585  geoisum1c  12586  cvgrat  12589  mertenslem2  12591  mertens  12592  eftval  12608  efval  12611  efcvgfsum  12617  ege2le3  12621  eftlub  12639  eflegeo  12651  sinval  12652  cosval  12653  tanval  12658  eirrlem  12732  rpnnen2lem1  12743  rpnnen2lem2  12744  bitsfval  12864  bitsinv2  12884  bitsinv  12889  sadcf  12894  sadc0  12895  sadcp1  12896  smupf  12919  smup0  12920  smupp1  12921  qnumval  13058  qdenval  13059  phival  13085  crt  13096  phimullem  13097  eulerthlem2  13100  odzval  13106  iserodd  13138  pcmpt  13190  prmreclem1  13213  prmreclem2  13214  prmreclem4  13216  prmreclem5  13217  prmreclem6  13218  1arithlem1  13220  1arithlem2  13221  vdwapfval  13268  vdwlem2  13279  vdwlem6  13283  vdwlem8  13285  vdwlem9  13286  ramub1lem2  13324  ramcl  13326  strfvnd  13413  topnval  13591  prdsplusgfval  13625  prdsmulrfval  13627  isacs  13805  acsfn  13813  cidfval  13830  homffval  13846  comfffval  13853  oppcval  13868  monfval  13887  oppcmon  13893  sectffval  13905  invffval  13912  isoval  13919  idfuval  14002  homafval  14113  arwval  14127  idafval  14141  coafval  14148  yonedainv  14307  pltfval  14345  lubfval  14364  lubval  14365  glbfval  14369  glbval  14370  joinfval  14373  meetfval  14380  p0val  14399  p1val  14400  oduval  14486  ipoval  14509  plusffval  14631  grpidval  14636  issubm  14677  prdspjmhm  14695  grpinvfval  14772  grpinvval  14773  grpsubfval  14776  grplactfval  14814  grplactval  14815  mulgfval  14820  prdsinvlem  14855  pwsmulg  14861  issubg  14873  cycsubgcl  14895  isnsg  14898  conjghm  14965  conjnmz  14968  symgval  15023  cntrval  15047  cntzfval  15048  cntzval  15049  oppgval  15072  odfval  15100  odval  15101  sylow1lem4  15164  pgpssslw  15177  sylow2blem3  15185  sylow3lem2  15191  lsmfval  15201  pj1fval  15255  efgval  15278  efgsval  15292  frgpval  15319  vrgpval  15328  mulgmhm  15379  mulgghm  15380  ablfaclem1  15572  mgpval  15580  rnglghm  15640  rngrghm  15641  opprval  15658  dvdsrval  15679  isunit  15691  invrfval  15707  dvrfval  15718  isirred  15733  issubrg  15797  abvfval  15835  abvtrivd  15857  staffval  15864  stafval  15865  scaffval  15897  lmodvsghm  15934  lssset  15939  lspfval  15978  islbs  16077  sraval  16177  rlmval  16193  2idlval  16233  lpival  16245  rrgval  16276  fidomndrnglem  16295  aspval  16316  asclfval  16322  asclval  16323  psrmulval  16379  psrlidm  16396  psrridm  16397  mvrval  16414  mvrval2  16415  mplmonmul  16456  psr1val  16513  vr1val  16519  ply1val  16521  coe1fval  16532  coe1fv  16533  coe1tmmul2  16597  coe1tmmul  16598  coe1tmmul2fv  16599  coe1pwmulfv  16601  expmhm  16701  expghm  16702  mulgghm2  16711  mulgrhm  16712  zrhval  16714  zrhmulg  16716  zlmval  16722  chrval  16731  znval  16741  znzrhval  16752  ip0l  16792  ipffval  16804  ocvfval  16818  ocvval  16819  cssval  16834  thlval  16847  pjfval  16858  pjval  16862  isobs  16872  ordtval  17177  cnpval  17224  ptpjpre1  17526  ptpjopn  17567  dfac14  17573  upxp  17578  uptx  17580  hauseqlcld  17601  txlm  17603  xkoptsub  17609  xkoinjcn  17642  kqval  17681  xpstopnlem1  17764  fmval  17898  flfval  17945  ptcmplem2  18007  ptcmplem3  18008  symgtgp  18054  divstgpopn  18072  ussval  18212  iscfilu  18241  ismet  18264  isxmet  18265  mopnval  18360  prdsxmslem2  18451  nmfval  18509  nmval  18510  nmoval  18622  metdsval  18750  divcn  18771  mulc1cncf  18808  icopnfhmeo  18841  iccpnfhmeo  18843  xrhmeo  18844  cnheiborlem  18852  evth  18857  evth2  18858  lebnumlem3  18861  isphtpy  18879  isphtpc  18892  pcofval  18908  pcovalg  18910  pco1  18913  pcopt  18920  pcopt2  18921  pcoass  18922  pcorevcl  18923  pcorevlem  18924  pcorev2  18926  pi1xfrcnv  18955  cphnm  19029  tchval  19050  tchnmval  19060  cfilfval  19090  iscmet  19110  iscmet3lem3  19116  ivth2  19221  ovolval  19239  ovollb2lem  19253  ovolunlem1a  19261  ovolunlem1  19262  ovoliunlem1  19267  ovoliunlem2  19268  ovolicc1  19281  voliunlem1  19313  voliunlem2  19314  voliunlem3  19315  volsup  19319  ioorval  19335  uniioombllem3  19346  uniioombllem6  19349  volsup2  19366  volcn  19367  volivth  19368  vitalilem2  19370  vitalilem3  19371  vitalilem4  19372  vitali  19374  mbfmax  19410  mbfimaopnlem  19416  itg1val  19444  i1f1lem  19450  itg11  19452  itg1addlem4  19460  itg1mulc  19465  i1fres  19466  itg1climres  19475  mbfi1fseqlem2  19477  mbfi1fseqlem3  19478  mbfi1fseqlem6  19481  mbfi1flimlem  19483  mbfi1flim  19484  mbfmullem2  19485  itg2seq  19503  itg2uba  19504  itg2splitlem  19509  itg2monolem1  19511  itg2monolem2  19512  itg2monolem3  19513  itg2mono  19514  itg2i1fseqle  19515  itg2i1fseq  19516  itg2i1fseq2  19517  itg2addlem  19519  itg2cnlem1  19522  itg2cn  19524  limccnp2  19648  dvnff  19678  dvnp1  19680  cpnfval  19687  elcpn  19689  dvrec  19710  dvcnvlem  19729  dveflem  19732  dvef  19733  dvferm1  19738  dvferm2  19740  rolle  19743  dvlip  19746  dvlipcn  19747  dv11cn  19754  dvivthlem1  19761  dvivth  19763  lhop1lem  19766  ftc1lem1  19788  ftc1lem5  19793  ftc2  19797  itgsubstlem  19801  evlslem3  19804  evlslem1  19805  evlsval  19809  evlssca  19812  evlsvar  19813  evl1fval  19816  evl1val  19817  tdeglem3  19851  tdeglem4  19852  mdegval  19855  mdegmullem  19870  deg1fval  19872  deg1ldg  19884  deg1leb  19887  coe1mul3  19891  uc1pval  19931  mon1pval  19933  q1pval  19945  r1pval  19948  ply1remlem  19954  ig1pval  19964  plyval  19981  elply2  19984  plyeq0lem  19998  coeval  20011  dgrval  20016  coeid2  20027  coemullem  20037  coemul  20039  elqaalem1  20105  elqaalem2  20106  elqaalem3  20107  iaa  20111  aareccl  20112  aannenlem1  20114  geolim3  20125  aaliou3lem1  20128  aaliou3lem2  20129  aaliou3lem5  20133  aaliou3lem6  20134  aaliou3lem7  20135  aaliou3  20137  tayl0  20147  taylthlem1  20158  taylthlem2  20159  ulmshftlem  20174  ulmshft  20175  ulmuni  20177  ulmcau  20180  ulmdvlem1  20185  ulmdvlem3  20187  mtest  20189  mtestbdd  20190  mbfulm  20191  iblulm  20192  itgulm  20193  pserval  20195  pserval2  20196  radcnvlem1  20198  radcnvlem2  20199  dvradcnv  20206  pserulm  20207  pserdvlem2  20213  pserdv  20214  abelthlem1  20216  abelthlem3  20218  abelthlem4  20219  abelthlem5  20220  abelthlem6  20221  abelthlem7  20223  abelthlem8  20224  abelthlem9  20225  resinf1o  20307  efgh  20312  efif1olem4  20316  eff1olem  20319  logcnlem5  20406  logtayllem  20419  logtayl  20420  logtaylsum  20421  logtayl2  20422  logccv  20423  asinval  20591  acosval  20592  atanval  20593  atantayl  20646  leibpilem2  20650  leibpi  20651  leibpisum  20652  log2cnv  20653  log2tlbnd  20654  areaval  20672  efrlim  20677  dfef2  20678  amgmlem  20697  emcllem2  20704  emcllem3  20705  emcllem4  20706  emcllem5  20707  emcllem6  20708  emcllem7  20709  ftalem7  20730  basellem2  20733  basellem3  20734  basellem4  20735  basellem5  20736  basellem6  20737  basellem8  20739  basellem9  20740  chtval  20762  vmaval  20765  chpval  20774  ppival  20779  muval  20784  prmorcht  20830  sqff1o  20834  dvdsflsumcom  20842  musum  20845  muinv  20847  sgmppw  20850  fsumvma  20866  pclogsum  20868  dchrfi  20908  bposlem5  20941  bposlem7  20943  bposlem8  20944  bposlem9  20945  lgsfval  20954  lgsdir  20983  lgsdilem2  20984  lgsdi  20985  lgsne0  20986  lgsqrlem2  20995  lgsqrlem4  20997  lgseisenlem2  21003  dchrmusum2  21057  dchrvmasumlem1  21058  dchrvmasumiflem1  21064  dchrvmaeq0  21067  dchrisum0fval  21068  dchrisum0re  21076  mulog2sumlem1  21097  pntrval  21125  pntsval  21135  pntrlog2bndlem4  21143  pntrlog2bndlem5  21144  pntlem3  21172  abvcxp  21178  padicfval  21179  padicval  21180  padicabv  21193  ostth1  21196  ostth2  21200  ostth3  21201  vdgrval  21517  gidval  21651  grpoinvval  21663  bafval  21933  imsval  22027  dipfval  22048  sspval  22072  nmooval  22114  hmoval  22161  ipasslem8  22188  ipasslem9  22189  ipblnfi  22207  ubthlem2  22223  htthlem  22270  normval  22476  ocval  22632  occllem  22655  hsupval  22686  pjhfval  22748  pjhval  22749  chscllem2  22990  chscllem3  22991  hosval  23093  homval  23094  hodval  23095  hfsval  23096  hfmval  23097  brafval  23296  braval  23297  kbval  23307  eigvalval  23313  cnlnadjlem1  23420  nmopadjlei  23441  hmopidmchi  23504  strlem2  23604  hstrlem2  23612  cdj3lem2  23788  rmulccn  24120  xrmulc1cn  24122  xrge0iifcv  24126  xrge0iifiso  24127  xrge0iifhom  24129  xrge0iif1  24130  qqhval  24159  rrhval  24180  sxbrsigalem0  24417  sxbrsigalem3  24418  rrvmbfm  24481  dstrvval  24509  coinflippv  24522  ballotlem2  24527  ballotlemfval  24528  ballotlemi  24539  ballotlemsval  24547  ballotlemrval  24556  ballotth  24576  zetacvg  24580  lgamgulmlem4  24597  lgamgulmlem5  24598  lgamgulm2  24601  lgamcvglem  24605  igamval  24612  lgamcvg2  24620  gamcvg2lem  24624  derangval  24634  subfacval  24640  erdszelem3  24660  erdszelem9  24666  erdszelem10  24667  txpcon  24700  indispcon  24702  cvxpcon  24710  cvmlift2lem2  24772  cvmlift2lem3  24773  cvmlift2lem7  24777  cvmliftphtlem  24785  cvmlift3lem4  24790  snmlfval  24798  snmlval  24799  sinccvglem  24890  circum  24892  divcnvshft  24992  divcnvlin  24993  prodfdiv  25005  fprodser  25056  fprodshft  25081  fprodrev  25082  iprodmul  25090  faclimlem1  25122  faclimlem2  25123  faclim  25125  iprodfac  25126  faclim2  25127  dfrdg2  25178  elee  25549  axsegconlem1  25572  axsegconlem9  25580  axsegconlem10  25581  axpasch  25596  axlowdimlem15  25611  axlowdim  25616  axeuclidlem  25617  axcontlem2  25620  bpolylem  25810  findabrcl  25920  voliunnfl  25957  volsupnfl  25958  itg2addnclem  25959  itg2addnc  25961  ftc1cnnc  25981  fvopabf4g  26115  sdclem2  26139  fdc  26142  lmclim2  26157  geomcau  26158  istotbnd  26171  isbnd  26182  prdsbnd2  26197  heiborlem6  26218  heiborlem7  26219  heiborlem8  26220  rrnval  26229  rrncmslem  26234  idlval  26316  pridlval  26336  maxidlval  26342  isnacs  26451  mzpclval  26475  mzpsubst  26498  mzprename  26499  mzpcompact2lem  26501  eldiophb  26508  diophrw  26510  eldioph2  26513  diophin  26524  diophun  26525  diophren  26567  pell1qrval  26602  pell14qrval  26604  pell1234qrval  26606  pellfundval  26636  rmxypairf1o  26667  rmxyval  26671  mzpcong  26730  pw2f1ocnv  26801  dnnumch1  26812  dfac11  26831  prdsinvgd2  26879  uvcresum  26913  frlmup1  26921  frlmup2  26922  islinds  26950  islindf5  26980  hbtlem1  26998  hbtlem7  27000  elmnc  27012  dgraaval  27020  mpaaval  27027  itgoval  27037  rgspnval  27044  flcidc  27050  psgnfval  27094  psgnval  27101  mamulid  27129  mamurid  27130  mdetleib  27159  mendval  27162  issdrg  27176  phisum  27189  mon1pid  27195  cytpval  27199  lhe4.4ex1a  27217  addrfv  27344  subrfv  27345  mulvfv  27346  itgsin0pilem1  27414  stoweidlem55  27474  wallispilem1  27484  wallispilem2  27485  wallispilem4  27487  wallispi2lem1  27490  wallispi2lem2  27491  sinhval-named  27827  coshval-named  27828  tanhval-named  27829  secval  27838  cscval  27839  cotval  27840  sgnval  27866  ceilingval  27876  lshpset  29095  lsatset  29107  lcvfbr  29137  lflset  29176  lflnegcl  29192  lkrfval  29204  lshpkrlem1  29227  lshpkrlem2  29228  lshpkrlem3  29229  ldualset  29242  cmtfvalN  29327  cvrfval  29385  pats  29402  llnset  29621  lplnset  29645  lvolset  29688  lineset  29854  pointsetN  29857  psubspset  29860  pmapfval  29872  pmapval  29873  paddfval  29913  pclfvalN  30005  polfvalN  30020  polvalN  30021  psubclsetN  30052  watfvalN  30108  watvalN  30109  lhpset  30111  lautset  30198  pautsetN  30214  ldilfset  30224  ldilset  30225  ltrnfset  30233  ltrnset  30234  dilfsetN  30268  dilsetN  30269  trnfsetN  30271  trnsetN  30272  trlfset  30276  trlset  30277  trlval  30278  tgrpfset  30860  tgrpset  30861  tendofset  30874  tendoset  30875  tendo02  30903  tendoi  30910  erngfset  30915  erngset  30916  erngfset-rN  30923  erngset-rN  30924  cdlemksv  30960  dvafset  31120  dvaset  31121  dvaplusgv  31126  diaffval  31147  diafval  31148  diaval  31149  dvhfset  31197  dvhset  31198  cdlemm10N  31235  docaffvalN  31238  docafvalN  31239  djaffvalN  31250  djafvalN  31251  dibffval  31257  dibfval  31258  dibval  31259  dicffval  31291  dicfval  31292  dicval  31293  dihffval  31347  dihfval  31348  dihval  31349  dochffval  31466  dochfval  31467  djhffval  31513  djhfval  31514  dochfl1  31593  lpolsetN  31599  lcfrlem8  31666  lcdfval  31705  lcdval  31706  mapdffval  31743  mapdfval  31744  mapdhval  31841  hvmapffval  31875  hvmapfval  31876  hdmap1ffval  31913  hdmap1fval  31914  hdmapffval  31946  hdmapfval  31947  hgmapffval  32005  hgmapfval  32006
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
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 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-iota 5360  df-fun 5398  df-fv 5404
  Copyright terms: Public domain W3C validator