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

Theorem fvmpt 5835
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 5833 . 2  |-  ( ( A  e.  D  /\  C  e.  _V )  ->  ( F `  A
)  =  C )
51, 4mpan2 654 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1727   _Vcvv 2962    e. cmpt 4291   ` cfv 5483
This theorem is referenced by:  fvmptex  5844  fvresex  6011  ofval  6343  caofinvl  6360  1stval  6380  2ndval  6381  reldm  6427  curry1val  6468  curry2val  6472  fnwelem  6490  brtpos2  6514  onovuni  6633  tz7.44-1  6693  oasuc  6797  oesuclem  6798  omsuc  6799  onasuc  6801  onmsuc  6802  fvmptmap  7079  xpcomco  7227  unxpdomlem1  7342  unfilem2  7401  ordtypelem3  7518  ixpiunwdom  7588  inf3lema  7608  noinfep  7643  cantnfval  7652  cantnflem1d  7673  cantnflem1  7674  r1sucg  7724  r0weon  7925  infxpenc2lem1  7931  fseqenlem1  7936  fseqenlem2  7937  dfac8alem  7941  ac5num  7948  acni2  7958  dfac4  8034  dfac2a  8041  dfacacn  8052  dfac12lem1  8054  ackbij1lem7  8137  ackbij2lem2  8151  ackbij2lem3  8152  cfsmolem  8181  fin23lem28  8251  fin23lem39  8261  isf32lem6  8269  isf32lem7  8270  isf32lem8  8271  fin1a2lem3  8313  itunifval  8327  itunisuc  8330  axdc2lem  8359  axdc3lem2  8362  axcclem  8368  zorn2lem1  8407  negiso  10015  infmsup  10017  uzval  10521  flval  11234  monoord2  11385  seqf1olem2  11394  seqf1o  11395  seqdistr  11405  serle  11409  seqof  11411  swrdfv  11802  revval  11823  revfv  11826  cjval  11938  reval  11942  imval  11943  sqrval  12073  absval  12074  limsupval  12299  limsupgval  12301  climmpt  12396  climle  12464  rlimdiv  12470  isercolllem1  12489  isercoll2  12493  caurcvg2  12502  fsumser  12555  isumadd  12582  fsumcnv  12588  fsumrev  12593  fsumshft  12594  iserabs  12625  cvgcmp  12626  cvgcmpce  12628  incexclem  12647  isumless  12656  supcvg  12666  harmonic  12669  trireciplem  12672  trirecip  12673  expcnv  12674  explecnv  12675  geolim  12678  geolim2  12679  geo2lim  12683  geomulcvg  12684  geoisum  12685  geoisumr  12686  geoisum1  12687  geoisum1c  12688  cvgrat  12691  mertenslem2  12693  mertens  12694  eftval  12710  efval  12713  efcvgfsum  12719  ege2le3  12723  eftlub  12741  eflegeo  12753  sinval  12754  cosval  12755  tanval  12760  eirrlem  12834  rpnnen2lem1  12845  rpnnen2lem2  12846  bitsfval  12966  bitsinv2  12986  bitsinv  12991  sadcf  12996  sadc0  12997  sadcp1  12998  smupf  13021  smup0  13022  smupp1  13023  qnumval  13160  qdenval  13161  phival  13187  crt  13198  phimullem  13199  eulerthlem2  13202  odzval  13208  iserodd  13240  pcmpt  13292  prmreclem1  13315  prmreclem2  13316  prmreclem4  13318  prmreclem5  13319  prmreclem6  13320  1arithlem1  13322  1arithlem2  13323  vdwapfval  13370  vdwlem2  13381  vdwlem6  13385  vdwlem8  13387  vdwlem9  13388  ramub1lem2  13426  ramcl  13428  strfvnd  13515  topnval  13693  prdsplusgfval  13727  prdsmulrfval  13729  isacs  13907  acsfn  13915  cidfval  13932  homffval  13948  comfffval  13955  oppcval  13970  monfval  13989  oppcmon  13995  sectffval  14007  invffval  14014  isoval  14021  idfuval  14104  homafval  14215  arwval  14229  idafval  14243  coafval  14250  yonedainv  14409  pltfval  14447  lubfval  14466  lubval  14467  glbfval  14471  glbval  14472  joinfval  14475  meetfval  14482  p0val  14501  p1val  14502  oduval  14588  ipoval  14611  plusffval  14733  grpidval  14738  issubm  14779  prdspjmhm  14797  grpinvfval  14874  grpinvval  14875  grpsubfval  14878  grplactfval  14916  grplactval  14917  mulgfval  14922  prdsinvlem  14957  pwsmulg  14963  issubg  14975  cycsubgcl  14997  isnsg  15000  conjghm  15067  conjnmz  15070  symgval  15125  cntrval  15149  cntzfval  15150  cntzval  15151  oppgval  15174  odfval  15202  odval  15203  sylow1lem4  15266  pgpssslw  15279  sylow2blem3  15287  sylow3lem2  15293  lsmfval  15303  pj1fval  15357  efgval  15380  efgsval  15394  frgpval  15421  vrgpval  15430  mulgmhm  15481  mulgghm  15482  ablfaclem1  15674  mgpval  15682  rnglghm  15742  rngrghm  15743  opprval  15760  dvdsrval  15781  isunit  15793  invrfval  15809  dvrfval  15820  isirred  15835  issubrg  15899  abvfval  15937  abvtrivd  15959  staffval  15966  stafval  15967  scaffval  15999  lmodvsghm  16036  lssset  16041  lspfval  16080  islbs  16179  sraval  16279  rlmval  16295  2idlval  16335  lpival  16347  rrgval  16378  fidomndrnglem  16397  aspval  16418  asclfval  16424  asclval  16425  psrmulval  16481  psrlidm  16498  psrridm  16499  mvrval  16516  mvrval2  16517  mplmonmul  16558  psr1val  16615  vr1val  16621  ply1val  16623  coe1fval  16634  coe1fv  16635  coe1tmmul2  16699  coe1tmmul  16700  coe1tmmul2fv  16701  coe1pwmulfv  16703  expmhm  16807  expghm  16808  mulgghm2  16817  mulgrhm  16818  zrhval  16820  zrhmulg  16822  zlmval  16828  chrval  16837  znval  16847  znzrhval  16858  ip0l  16898  ipffval  16910  ocvfval  16924  ocvval  16925  cssval  16940  thlval  16953  pjfval  16964  pjval  16968  isobs  16978  ordtval  17284  cnpval  17331  ptpjpre1  17634  ptpjopn  17675  dfac14  17681  upxp  17686  uptx  17688  hauseqlcld  17709  txlm  17711  xkoptsub  17717  xkoinjcn  17750  kqval  17789  xpstopnlem1  17872  fmval  18006  flfval  18053  ptcmplem2  18115  ptcmplem3  18116  symgtgp  18162  divstgpopn  18180  ussval  18320  iscfilu  18349  ispsmet  18366  ismet  18384  isxmet  18385  mopnval  18499  prdsxmslem2  18590  nmfval  18667  nmval  18668  nmoval  18780  metdsval  18908  divcn  18929  mulc1cncf  18966  icopnfhmeo  18999  iccpnfhmeo  19001  xrhmeo  19002  cnheiborlem  19010  evth  19015  evth2  19016  lebnumlem3  19019  isphtpy  19037  isphtpc  19050  pcofval  19066  pcovalg  19068  pco1  19071  pcopt  19078  pcopt2  19079  pcoass  19080  pcorevcl  19081  pcorevlem  19082  pcorev2  19084  pi1xfrcnv  19113  cphnm  19187  tchval  19208  tchnmval  19218  cfilfval  19248  iscmet  19268  iscmet3lem3  19274  ivth2  19383  ovolval  19401  ovollb2lem  19415  ovolunlem1a  19423  ovolunlem1  19424  ovoliunlem1  19429  ovoliunlem2  19430  ovolicc1  19443  voliunlem1  19475  voliunlem2  19476  voliunlem3  19477  volsup  19481  ioorval  19497  uniioombllem3  19508  uniioombllem6  19511  volsup2  19528  volcn  19529  volivth  19530  vitalilem2  19532  vitalilem3  19533  vitalilem4  19534  vitali  19536  mbfmax  19570  mbfimaopnlem  19576  itg1val  19604  i1f1lem  19610  itg11  19612  itg1addlem4  19620  itg1mulc  19625  i1fres  19626  itg1climres  19635  mbfi1fseqlem2  19637  mbfi1fseqlem3  19638  mbfi1fseqlem6  19641  mbfi1flimlem  19643  mbfi1flim  19644  mbfmullem2  19645  itg2seq  19663  itg2uba  19664  itg2splitlem  19669  itg2monolem1  19671  itg2monolem2  19672  itg2monolem3  19673  itg2mono  19674  itg2i1fseqle  19675  itg2i1fseq  19676  itg2i1fseq2  19677  itg2addlem  19679  itg2cnlem1  19682  itg2cn  19684  limccnp2  19810  dvnff  19840  dvnp1  19842  cpnfval  19849  elcpn  19851  dvrec  19872  dvcnvlem  19891  dveflem  19894  dvef  19895  dvferm1  19900  dvferm2  19902  rolle  19905  dvlip  19908  dvlipcn  19909  dv11cn  19916  dvivthlem1  19923  dvivth  19925  lhop1lem  19928  ftc1lem1  19950  ftc1lem5  19955  ftc2  19959  itgsubstlem  19963  evlslem3  19966  evlslem1  19967  evlsval  19971  evlssca  19974  evlsvar  19975  evl1fval  19978  evl1val  19979  tdeglem3  20013  tdeglem4  20014  mdegval  20017  mdegmullem  20032  deg1fval  20034  deg1ldg  20046  deg1leb  20049  coe1mul3  20053  uc1pval  20093  mon1pval  20095  q1pval  20107  r1pval  20110  ply1remlem  20116  ig1pval  20126  plyval  20143  elply2  20146  plyeq0lem  20160  coeval  20173  dgrval  20178  coeid2  20189  coemullem  20199  coemul  20201  elqaalem1  20267  elqaalem2  20268  elqaalem3  20269  iaa  20273  aareccl  20274  aannenlem1  20276  geolim3  20287  aaliou3lem1  20290  aaliou3lem2  20291  aaliou3lem5  20295  aaliou3lem6  20296  aaliou3lem7  20297  aaliou3  20299  tayl0  20309  taylthlem1  20320  taylthlem2  20321  ulmshftlem  20336  ulmshft  20337  ulmuni  20339  ulmcau  20342  ulmdvlem1  20347  ulmdvlem3  20349  mtest  20351  mtestbdd  20352  mbfulm  20353  iblulm  20354  itgulm  20355  pserval  20357  pserval2  20358  radcnvlem1  20360  radcnvlem2  20361  dvradcnv  20368  pserulm  20369  pserdvlem2  20375  pserdv  20376  abelthlem1  20378  abelthlem3  20380  abelthlem4  20381  abelthlem5  20382  abelthlem6  20383  abelthlem7  20385  abelthlem8  20386  abelthlem9  20387  resinf1o  20469  efgh  20474  efif1olem4  20478  eff1olem  20481  logcnlem5  20568  logtayllem  20581  logtayl  20582  logtaylsum  20583  logtayl2  20584  logccv  20585  asinval  20753  acosval  20754  atanval  20755  atantayl  20808  leibpilem2  20812  leibpi  20813  leibpisum  20814  log2cnv  20815  log2tlbnd  20816  areaval  20834  efrlim  20839  dfef2  20840  amgmlem  20859  emcllem2  20866  emcllem3  20867  emcllem4  20868  emcllem5  20869  emcllem6  20870  emcllem7  20871  ftalem7  20892  basellem2  20895  basellem3  20896  basellem4  20897  basellem5  20898  basellem6  20899  basellem8  20901  basellem9  20902  chtval  20924  vmaval  20927  chpval  20936  ppival  20941  muval  20946  prmorcht  20992  sqff1o  20996  dvdsflsumcom  21004  musum  21007  muinv  21009  sgmppw  21012  fsumvma  21028  pclogsum  21030  dchrfi  21070  bposlem5  21103  bposlem7  21105  bposlem8  21106  bposlem9  21107  lgsfval  21116  lgsdir  21145  lgsdilem2  21146  lgsdi  21147  lgsne0  21148  lgsqrlem2  21157  lgsqrlem4  21159  lgseisenlem2  21165  dchrmusum2  21219  dchrvmasumlem1  21220  dchrvmasumiflem1  21226  dchrvmaeq0  21229  dchrisum0fval  21230  dchrisum0re  21238  mulog2sumlem1  21259  pntrval  21287  pntsval  21297  pntrlog2bndlem4  21305  pntrlog2bndlem5  21306  pntlem3  21334  abvcxp  21340  padicfval  21341  padicval  21342  padicabv  21355  ostth1  21358  ostth2  21362  ostth3  21363  vdgrval  21698  gidval  21832  grpoinvval  21844  bafval  22114  imsval  22208  dipfval  22229  sspval  22253  nmooval  22295  hmoval  22342  ipasslem8  22369  ipasslem9  22370  ipblnfi  22388  ubthlem2  22404  htthlem  22451  normval  22657  ocval  22813  occllem  22836  hsupval  22867  pjhfval  22929  pjhval  22930  chscllem2  23171  chscllem3  23172  hosval  23274  homval  23275  hodval  23276  hfsval  23277  hfmval  23278  brafval  23477  braval  23478  kbval  23488  eigvalval  23494  cnlnadjlem1  23601  nmopadjlei  23622  hmopidmchi  23685  strlem2  23785  hstrlem2  23793  cdj3lem2  23969  ofpreima  24112  inftmrel  24281  isinftm  24282  rmulccn  24345  xrmulc1cn  24347  xrge0iifcv  24351  xrge0iifiso  24352  xrge0iifhom  24354  xrge0iif1  24355  qqhval  24389  rrhval  24410  xrhval  24415  sxbrsigalem0  24652  sxbrsigalem3  24653  rrvmbfm  24731  dstrvval  24759  coinflippv  24772  ballotlem2  24777  ballotlemfval  24778  ballotlemi  24789  ballotlemsval  24797  ballotlemrval  24806  ballotth  24826  zetacvg  24830  lgamgulmlem4  24847  lgamgulmlem5  24848  lgamgulm2  24851  lgamcvglem  24855  igamval  24862  lgamcvg2  24870  gamcvg2lem  24874  derangval  24884  subfacval  24890  erdszelem3  24910  erdszelem9  24916  erdszelem10  24917  txpcon  24950  indispcon  24952  cvxpcon  24960  cvmlift2lem2  25022  cvmlift2lem3  25023  cvmlift2lem7  25027  cvmliftphtlem  25035  cvmlift3lem4  25040  snmlfval  25048  snmlval  25049  sinccvglem  25140  circum  25142  divcnvshft  25242  divcnvlin  25243  prodfdiv  25255  fprodser  25306  fprodshft  25331  fprodrev  25332  fprodcnv  25338  iprodmul  25347  iprodefisum  25349  iprodgam  25350  faclimlem1  25393  faclimlem2  25394  faclim  25396  iprodfac  25397  faclim2  25398  dfrdg2  25454  elee  25864  axsegconlem1  25887  axsegconlem9  25895  axsegconlem10  25896  axpasch  25911  axlowdimlem15  25926  axlowdim  25931  axeuclidlem  25932  axcontlem2  25935  bpolylem  26125  findabrcl  26235  mblfinlem2  26280  voliunnfl  26286  volsupnfl  26287  itg2addnclem  26294  itg2addnclem3  26296  ftc1cnnc  26317  ftc1anclem5  26322  ftc1anclem6  26323  ftc1anclem7  26324  ftc1anc  26326  ftc2nc  26327  fvopabf4g  26460  sdclem2  26484  fdc  26487  lmclim2  26502  geomcau  26503  istotbnd  26516  isbnd  26527  prdsbnd2  26542  heiborlem6  26563  heiborlem7  26564  heiborlem8  26565  rrnval  26574  rrncmslem  26579  idlval  26661  pridlval  26681  maxidlval  26687  isnacs  26796  mzpclval  26820  mzpsubst  26843  mzprename  26844  mzpcompact2lem  26846  eldiophb  26853  diophrw  26855  eldioph2  26858  diophin  26869  diophun  26870  diophren  26912  pell1qrval  26947  pell14qrval  26949  pell1234qrval  26951  pellfundval  26981  rmxypairf1o  27012  rmxyval  27016  mzpcong  27075  pw2f1ocnv  27146  dnnumch1  27157  dfac11  27175  prdsinvgd2  27223  uvcresum  27257  frlmup1  27265  frlmup2  27266  islinds  27294  islindf5  27324  hbtlem1  27342  hbtlem7  27344  elmnc  27356  dgraaval  27364  mpaaval  27371  itgoval  27381  rgspnval  27388  flcidc  27394  psgnfval  27438  psgnval  27445  mamulid  27473  mamurid  27474  mdetleib  27503  mendval  27506  issdrg  27520  phisum  27533  mon1pid  27539  cytpval  27543  lhe4.4ex1a  27561  addrfv  27688  subrfv  27689  mulvfv  27690  itgsin0pilem1  27758  stoweidlem55  27818  wallispilem1  27828  wallispilem2  27829  wallispilem4  27831  wallispi2lem1  27834  wallispi2lem2  27835  sinhval-named  28577  coshval-named  28578  tanhval-named  28579  secval  28588  cscval  28589  cotval  28590  sgnval  28616  ceilingval  28626  lshpset  29874  lsatset  29886  lcvfbr  29916  lflset  29955  lflnegcl  29971  lkrfval  29983  lshpkrlem1  30006  lshpkrlem2  30007  lshpkrlem3  30008  ldualset  30021  cmtfvalN  30106  cvrfval  30164  pats  30181  llnset  30400  lplnset  30424  lvolset  30467  lineset  30633  pointsetN  30636  psubspset  30639  pmapfval  30651  pmapval  30652  paddfval  30692  pclfvalN  30784  polfvalN  30799  polvalN  30800  psubclsetN  30831  watfvalN  30887  watvalN  30888  lhpset  30890  lautset  30977  pautsetN  30993  ldilfset  31003  ldilset  31004  ltrnfset  31012  ltrnset  31013  dilfsetN  31047  dilsetN  31048  trnfsetN  31050  trnsetN  31051  trlfset  31055  trlset  31056  trlval  31057  tgrpfset  31639  tgrpset  31640  tendofset  31653  tendoset  31654  tendo02  31682  tendoi  31689  erngfset  31694  erngset  31695  erngfset-rN  31702  erngset-rN  31703  cdlemksv  31739  dvafset  31899  dvaset  31900  dvaplusgv  31905  diaffval  31926  diafval  31927  diaval  31928  dvhfset  31976  dvhset  31977  cdlemm10N  32014  docaffvalN  32017  docafvalN  32018  djaffvalN  32029  djafvalN  32030  dibffval  32036  dibfval  32037  dibval  32038  dicffval  32070  dicfval  32071  dicval  32072  dihffval  32126  dihfval  32127  dihval  32128  dochffval  32245  dochfval  32246  djhffval  32292  djhfval  32293  dochfl1  32372  lpolsetN  32378  lcfrlem8  32445  lcdfval  32484  lcdval  32485  mapdffval  32522  mapdfval  32523  mapdhval  32620  hvmapffval  32654  hvmapfval  32655  hdmap1ffval  32692  hdmap1fval  32693  hdmapffval  32725  hdmapfval  32726  hgmapffval  32784  hgmapfval  32785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-iota 5447  df-fun 5485  df-fv 5491
  Copyright terms: Public domain W3C validator