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

Theorem fvmpt 6503
Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
Hypotheses
Ref Expression
fvmptg.1 (𝑥 = 𝐴𝐵 = 𝐶)
fvmptg.2 𝐹 = (𝑥𝐷𝐵)
fvmpt.3 𝐶 ∈ V
Assertion
Ref Expression
fvmpt (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt
StepHypRef Expression
1 fvmpt.3 . 2 𝐶 ∈ V
2 fvmptg.1 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
3 fvmptg.2 . . 3 𝐹 = (𝑥𝐷𝐵)
42, 3fvmptg 6501 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 674 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156  Vcvv 3391  cmpt 4923  cfv 6101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-iota 6064  df-fun 6103  df-fv 6109
This theorem is referenced by:  fvmptex  6515  fvmptrabfv  6530  mptfvmpt  6715  ofval  7136  caofinvl  7154  fvresex  7369  1stval  7400  2ndval  7401  reldm  7451  curry1val  7504  curry2val  7508  fnwelem  7526  brtpos2  7593  onovuni  7675  tz7.44-1  7738  oasuc  7841  oesuclem  7842  omsuc  7843  onasuc  7845  onmsuc  7846  fvmptmap  8129  xpcomco  8289  unxpdomlem1  8403  unfilem2  8464  ordtypelem3  8664  ixpiunwdom  8735  inf3lema  8768  noinfep  8804  cantnfval  8812  cantnflem1d  8832  cantnflem1  8833  r1sucg  8879  r0weon  9118  infxpenc2lem1  9125  fseqenlem1  9130  fseqenlem2  9131  dfac8alem  9135  ac5num  9142  acni2  9152  dfac4  9228  dfac2a  9235  dfacacn  9248  dfac12lem1  9250  ackbij1lem7  9333  ackbij2lem2  9347  ackbij2lem3  9348  cfsmolem  9377  fin23lem28  9447  fin23lem39  9457  isf32lem6  9465  isf32lem7  9466  isf32lem8  9467  fin1a2lem3  9509  itunifval  9523  itunisuc  9526  axdc2lem  9555  axdc3lem2  9558  axcclem  9564  zorn2lem1  9603  negiso  11288  infrenegsup  11291  uzval  11906  flval  12819  ceilval  12863  ceilval2  12865  monoord2  13055  seqf1olem2  13064  seqf1o  13065  seqdistr  13075  serle  13079  seqof  13081  swrdfv  13647  revval  13733  revfv  13736  wwlktovf1  13925  wwlktovfo  13926  sgnval  14051  cjval  14065  reval  14069  imval  14070  sqrtval  14200  absval  14201  limsupval  14428  limsupgval  14430  climmpt  14525  climle  14593  rlimdiv  14599  isercolllem1  14618  isercoll2  14622  caurcvg2  14631  fsumser  14684  isumadd  14721  fsumcnv  14727  fsumrev  14733  fsumshft  14734  iserabs  14769  cvgcmp  14770  cvgcmpce  14772  incexclem  14790  isumless  14799  divcnvshft  14809  supcvg  14810  harmonic  14813  trireciplem  14816  trirecip  14817  expcnv  14818  explecnv  14819  geolim  14823  geolim2  14824  geo2lim  14828  geomulcvg  14829  geoisum  14830  geoisumr  14831  geoisum1  14832  geoisum1c  14833  cvgrat  14836  mertenslem2  14838  mertens  14839  prodfdiv  14849  fprodser  14900  fprodshft  14927  fprodrev  14928  fprodcnv  14934  iprodmul  14954  bpolylem  14999  eftval  15027  efval  15030  efcvgfsum  15036  ege2le3  15040  eftlub  15059  eflegeo  15071  sinval  15072  cosval  15073  tanval  15078  eirrlem  15152  rpnnen2lem1  15163  rpnnen2lem2  15164  bitsfval  15364  bitsinv2  15384  bitsinv  15389  sadcf  15394  sadc0  15395  sadcp1  15396  smupf  15419  smup0  15420  smupp1  15421  qnumval  15662  qdenval  15663  phival  15689  crth  15700  phimullem  15701  eulerthlem2  15704  phisum  15712  odzval  15713  iserodd  15757  pcmpt  15813  prmreclem1  15837  prmreclem2  15838  prmreclem4  15840  prmreclem5  15841  prmreclem6  15842  1arithlem1  15844  1arithlem2  15845  vdwapfval  15892  vdwlem2  15903  vdwlem6  15907  vdwlem8  15909  vdwlem9  15910  ramub1lem2  15948  ramcl  15950  strfvnd  16087  topnval  16300  prdsplusgfval  16339  prdsmulrfval  16341  isacs  16516  acsfn  16524  homffval  16554  comfffval  16562  oppcval  16577  monfval  16596  oppcmon  16602  sectffval  16614  invffval  16622  isoval  16629  idfuval  16740  homafval  16883  arwval  16897  coafval  16918  yonedainv  17126  pltfval  17164  lubfval  17183  lubval  17189  glbfval  17196  glbval  17202  p0val  17246  p1val  17247  oduval  17335  ipoval  17359  plusffval  17452  grpidval  17465  issubm  17552  prdspjmhm  17572  grpinvval  17666  grpsubfval  17669  grplactval  17722  prdsinvlem  17729  mulgfval  17747  pwsmulg  17789  issubg  17796  cycsubgcl  17822  isnsg  17825  conjghm  17893  conjnmz  17896  cntrval  17953  cntzfval  17954  cntzval  17955  oppgval  17978  symgval  18000  psgnfval  18121  psgnval  18128  odval  18154  sylow1lem4  18217  pgpssslw  18230  sylow2blem3  18238  sylow3lem2  18244  lsmfval  18254  pj1fval  18308  efgval  18331  efgsval  18345  frgpval  18372  vrgpval  18381  mulgmhm  18434  mulgghm  18435  ablfaclem1  18686  mgpval  18694  srglmhm  18737  srgrmhm  18738  ringlghm  18806  ringrghm  18807  opprval  18826  dvdsrval  18847  isunit  18859  invrfval  18875  dvrfval  18886  isirred  18901  issubrg  18984  abvfval  19022  abvtrivd  19044  staffval  19051  stafval  19052  scaffval  19085  lmodvsghm  19128  lssset  19138  lspfval  19180  islbs  19283  sraval  19385  rlmval  19400  2idlval  19442  lpival  19454  rrgval  19496  fidomndrnglem  19515  aspval  19537  asclval  19544  psrmulval  19595  psrlidm  19612  psrridm  19613  mvrval  19630  mvrval2  19631  mplmonmul  19673  evlslem3  19722  evlslem1  19723  evlsval  19727  evlssca  19730  evlsvar  19731  psr1val  19764  vr1val  19770  ply1val  19772  coe1fval  19783  coe1fv  19784  coe1tmmul2  19854  coe1tmmul  19855  coe1tmmul2fv  19856  coe1pwmulfv  19858  evls1val  19893  evl1fval  19900  evl1val  19901  expmhm  20023  expghm  20052  mulgghm2  20053  mulgrhm  20054  zrhval  20064  zrhmulg  20066  zlmval  20072  chrval  20081  znval  20091  znzrhval  20102  evpmss  20139  psgnevpmb  20140  ip0l  20191  ipffval  20203  ocvfval  20220  ocvval  20221  cssval  20236  thlval  20249  pjfval  20260  pjval  20264  isobs  20274  prdsinvgd2  20296  uvcresum  20342  frlmup1  20347  frlmup2  20348  islinds  20358  islindf5  20388  mamulid  20457  mamurid  20458  mdetleib  20604  mdetleib1  20608  mdetunilem9  20637  mdetuni0  20638  mdetmul  20640  cpmidpmatlem1  20888  ordtval  21207  cnpval  21254  ptpjpre1  21588  ptpjopn  21629  dfac14  21635  upxp  21640  uptx  21642  hauseqlcld  21663  txlm  21665  xkoptsub  21671  xkoinjcn  21704  kqval  21743  xpstopnlem1  21826  fmval  21960  flfval  22007  ptcmplem2  22070  ptcmplem3  22071  symgtgp  22118  qustgpopn  22136  ussval  22276  iscfilu  22305  ispsmet  22322  ismet  22341  isxmet  22342  mopnval  22456  prdsxmslem2  22547  nmfval  22606  nmval  22607  nmoval  22732  metdsval  22863  divcn  22884  mulc1cncf  22921  icopnfhmeo  22955  iccpnfhmeo  22957  xrhmeo  22958  cnheiborlem  22966  evth  22971  evth2  22972  lebnumlem3  22975  isphtpy  22993  isphtpc  23006  pcofval  23022  pcovalg  23024  pco1  23027  pcopt  23034  pcopt2  23035  pcoass  23036  pcorevcl  23037  pcorevlem  23038  pcorev2  23040  pi1xfrcnv  23069  cphnm  23205  tchval  23229  tchnmval  23240  cfilfval  23274  iscmet  23294  iscmet3lem3  23300  rrxval  23387  ehlval  23405  ivth2  23436  ovolval  23454  ovollb2lem  23469  ovolunlem1a  23477  ovolunlem1  23478  ovoliunlem1  23483  ovoliunlem2  23484  ovolicc1  23497  voliunlem1  23531  voliunlem2  23532  voliunlem3  23533  volsup  23537  ioorval  23555  uniioombllem3  23566  uniioombllem6  23569  volsup2  23586  volcn  23587  volivth  23588  vitalilem2  23590  vitalilem3  23591  vitalilem4  23592  vitali  23594  mbfmax  23630  mbfimaopnlem  23636  itg1val  23664  i1f1lem  23670  itg11  23672  itg1addlem4  23680  itg1mulc  23685  i1fres  23686  itg1climres  23695  mbfi1fseqlem2  23697  mbfi1fseqlem3  23698  mbfi1fseqlem6  23701  mbfi1flimlem  23703  mbfi1flim  23704  mbfmullem2  23705  itg2seq  23723  itg2uba  23724  itg2splitlem  23729  itg2monolem1  23731  itg2monolem2  23732  itg2monolem3  23733  itg2mono  23734  itg2i1fseqle  23735  itg2i1fseq  23736  itg2i1fseq2  23737  itg2addlem  23739  itg2cnlem1  23742  itg2cn  23744  limccnp2  23870  dvnff  23900  dvnp1  23902  cpnfval  23909  elcpn  23911  dvrec  23932  dvcnvlem  23953  dveflem  23956  dvef  23957  dvferm1  23962  dvferm2  23964  rolle  23967  dvlip  23970  dvlipcn  23971  dv11cn  23978  dvivthlem1  23985  dvivth  23987  lhop1lem  23990  ftc1lem1  24012  ftc1lem5  24017  ftc2  24021  itgsubstlem  24025  tdeglem3  24033  tdeglem4  24034  mdegval  24037  mdegmullem  24052  deg1fval  24054  deg1ldg  24066  deg1leb  24069  coe1mul3  24073  uc1pval  24113  mon1pval  24115  q1pval  24127  r1pval  24130  ply1remlem  24136  ig1pval  24146  plyval  24163  elply2  24166  plyeq0lem  24180  coeval  24193  dgrval  24198  coeid2  24209  coemullem  24220  coemul  24222  elqaalem1  24288  elqaalem2  24289  elqaalem3  24290  iaa  24294  aareccl  24295  aannenlem1  24297  geolim3  24308  aaliou3lem1  24311  aaliou3lem2  24312  aaliou3lem5  24316  aaliou3lem6  24317  aaliou3lem7  24318  aaliou3  24320  tayl0  24330  taylthlem1  24341  taylthlem2  24342  ulmshftlem  24357  ulmshft  24358  ulmuni  24360  ulmcau  24363  ulmdvlem1  24368  ulmdvlem3  24370  mtest  24372  mtestbdd  24373  mbfulm  24374  iblulm  24375  itgulm  24376  pserval  24378  pserval2  24379  radcnvlem1  24381  radcnvlem2  24382  dvradcnv  24389  pserulm  24390  pserdvlem2  24396  pserdv  24397  abelthlem1  24399  abelthlem3  24401  abelthlem4  24402  abelthlem5  24403  abelthlem6  24404  abelthlem7  24406  abelthlem8  24407  abelthlem9  24408  resinf1o  24497  efif1olem4  24506  eff1olem  24509  logcnlem5  24606  logtayllem  24619  logtayl  24620  logtaylsum  24621  logtayl2  24622  logccv  24623  asinval  24823  acosval  24824  atanval  24825  atantayl  24878  leibpilem2  24882  leibpi  24883  leibpisum  24884  log2cnv  24885  log2tlbnd  24886  areaval  24905  efrlim  24910  dfef2  24911  amgmlem  24930  emcllem2  24937  emcllem3  24938  emcllem4  24939  emcllem5  24940  emcllem6  24941  emcllem7  24942  zetacvg  24955  lgamgulmlem4  24972  lgamgulmlem5  24973  lgamgulm2  24976  lgamcvglem  24980  igamval  24987  lgamcvg2  24995  gamcvg2lem  24999  ftalem7  25019  basellem2  25022  basellem3  25023  basellem4  25024  basellem5  25025  basellem6  25026  basellem8  25028  basellem9  25029  chtval  25050  vmaval  25053  chpval  25062  ppival  25067  muval  25072  prmorcht  25118  sqff1o  25122  dvdsflsumcom  25128  musum  25131  muinv  25133  sgmppw  25136  fsumvma  25152  pclogsum  25154  dchrfi  25194  bposlem5  25227  bposlem7  25229  bposlem8  25230  bposlem9  25231  lgsfval  25241  lgsdir  25271  lgsdilem2  25272  lgsdi  25273  lgsne0  25274  lgsqrlem2  25286  lgsqrlem4  25288  lgseisenlem2  25315  dchrmusum2  25397  dchrvmasumlem1  25398  dchrvmasumiflem1  25404  dchrvmaeq0  25407  dchrisum0fval  25408  dchrisum0re  25416  mulog2sumlem1  25437  pntrval  25465  pntsval  25475  pntrlog2bndlem4  25483  pntrlog2bndlem5  25484  pntlem3  25512  abvcxp  25518  padicfval  25519  padicval  25520  padicabv  25533  ostth1  25536  ostth2  25540  ostth3  25541  iscgrg  25621  legval  25693  ishpg  25865  iscgra  25915  isinag  25943  isleag  25947  iseqlg  25961  ttgval  25969  elee  25988  axsegconlem1  26011  axsegconlem9  26019  axsegconlem10  26020  axpasch  26035  axlowdimlem15  26050  axlowdim  26055  axeuclidlem  26056  axcontlem2  26059  eengv  26073  vtxval  26092  iedgval  26093  vtxvalOLD  26094  iedgvalOLD  26095  vtxdgval  26592  wlknwwlksninjOLD  27016  wlknwwlksnsurOLD  27017  wlkwwlkinjOLD  27024  wlkwwlksurOLD  27025  wwlksnextinj  27036  wwlksnextsur  27037  clwwlkfv  27197  clwwlknonmpt2  27254  fusgreg2wsplem  27508  fusgreghash2wsp  27513  numclwwlk1lem2fv  27535  gidval  27695  grpoinvval  27706  bafval  27787  imsval  27868  dipfval  27885  sspval  27906  nmooval  27946  hmoval  27993  ipasslem8  28020  ipasslem9  28021  ipblnfi  28039  ubthlem2  28055  htthlem  28102  normval  28309  ocval  28467  occllem  28490  hsupval  28521  pjhfval  28583  pjhval  28584  chscllem2  28825  chscllem3  28826  hosval  28927  homval  28928  hodval  28929  hfsval  28930  hfmval  28931  brafval  29130  braval  29131  kbval  29141  eigvalval  29147  cnlnadjlem1  29254  nmopadjlei  29275  hmopidmchi  29338  strlem2  29438  hstrlem2  29446  cdj3lem2  29622  ofpreima  29792  inftmrel  30059  isinftm  30060  psgnfzto1stlem  30175  smatfval  30186  lmatval  30204  locfinreflem  30232  rmulccn  30299  xrmulc1cn  30301  xrge0iifcv  30305  xrge0iifiso  30306  xrge0iifhom  30308  xrge0iif1  30309  qqhval  30343  rrhval  30365  xrhval  30387  ddeval1  30622  ddeval0  30623  sxbrsigalem0  30658  sxbrsigalem3  30659  eulerpartlemgv  30760  rrvmbfm  30829  dstrvval  30857  coinflippv  30870  ballotlem2  30875  ballotlemfval  30876  ballotlemi  30887  ballotlemsval  30895  ballotlemrval  30904  ballotth  30924  plymulx  30950  signstfv  30965  signsvvfval  30980  derangval  31472  subfacval  31478  erdszelem3  31498  erdszelem9  31504  erdszelem10  31505  txpconn  31537  indispconn  31539  cvxpconn  31547  cvmlift2lem2  31609  cvmlift2lem3  31610  cvmlift2lem7  31614  cvmliftphtlem  31622  cvmlift3lem4  31627  snmlfval  31635  snmlval  31636  mvtval  31720  mrsubffval  31727  mrsubcv  31730  mrsubrn  31733  elmrsubrn  31740  msubffval  31743  mvhval  31754  mpstval  31755  mstaval  31764  mclsval  31783  mppsval  31792  sinccvglem  31888  circum  31890  divcnvlin  31940  iprodefisum  31949  iprodgam  31950  faclimlem1  31951  faclimlem2  31952  faclim  31954  iprodfac  31955  faclim2  31956  dfrdg2  32021  nosupfv  32173  findabrcl  32770  dnival  32778  bj-evalval  33338  bj-inftyexpiinv  33412  bj-inftyexpidisj  33414  curfv  33702  finixpnum  33707  poimirlem16  33738  poimir  33755  broucube  33756  mblfinlem2  33760  voliunnfl  33766  volsupnfl  33767  itg2addnclem  33773  itg2addnclem3  33775  ftc1cnnc  33796  ftc1anclem5  33801  ftc1anclem6  33802  ftc1anclem7  33803  ftc1anc  33805  ftc2nc  33806  fvopabf4g  33827  sdclem2  33849  fdc  33852  lmclim2  33865  geomcau  33866  istotbnd  33879  isbnd  33890  prdsbnd2  33905  heiborlem6  33926  heiborlem7  33927  heiborlem8  33928  rrnval  33937  rrncmslem  33942  idlval  34123  pridlval  34143  maxidlval  34149  lshpset  34758  lsatset  34770  lcvfbr  34800  lflset  34839  lflnegcl  34855  lshpkrlem1  34890  lshpkrlem2  34891  lshpkrlem3  34892  ldualset  34905  cmtfvalN  34990  cvrfval  35048  pats  35065  llnset  35285  lplnset  35309  lvolset  35352  lineset  35518  pointsetN  35521  psubspset  35524  pmapval  35537  paddfval  35577  pclfvalN  35669  polfvalN  35684  polvalN  35685  psubclsetN  35716  watvalN  35773  lhpset  35775  lautset  35862  pautsetN  35878  ldilset  35889  ltrnset  35898  dilsetN  35934  trnsetN  35937  trlset  35942  trlval  35943  tgrpset  36526  tendoset  36540  tendo02  36568  erngset  36581  erngset-rN  36589  cdlemksv  36625  dvaset  36786  dvaplusgv  36791  diafval  36812  diaval  36813  dvhset  36862  cdlemm10N  36899  docafvalN  36903  djafvalN  36915  dibfval  36922  dibval  36923  dicfval  36956  dicval  36957  dihval  37013  dochfval  37131  djhfval  37178  dochfl1  37257  lpolsetN  37263  lcdval  37370  mapdhval  37505  hvmapfval  37540  hdmap1fval  37577  isnacs  37769  mzpclval  37790  mzpsubst  37813  mzprename  37814  mzpcompact2lem  37816  eldiophb  37822  diophrw  37824  eldioph2  37827  diophin  37838  diophun  37839  diophren  37879  pell1qrval  37912  pell14qrval  37914  pell1234qrval  37916  pellfundval  37946  rmxypairf1o  37977  rmxyval  37981  mzpcong  38040  pw2f1ocnv  38105  dnnumch1  38115  dfac11  38133  hbtlem1  38194  hbtlem7  38196  elmnc  38207  dgraaval  38215  mpaaval  38222  itgoval  38232  rgspnval  38239  flcidc  38245  mendval  38254  issdrg  38268  mon1pid  38284  cytpval  38288  elcnvlem  38407  comptiunov2i  38498  dftrcl3  38512  trclfvcom  38515  cnvtrclfv  38516  cotrcltrcl  38517  trclimalb2  38518  trclfvdecomr  38520  dfrtrcl3  38525  dfrtrcl4  38530  clsk1indlem0  38839  clsk1indlem2  38840  clsk1indlem3  38841  clsk1indlem4  38842  clsk1indlem1  38843  k0004val  38948  lhe4.4ex1a  39028  addrfv  39171  subrfv  39172  mulvfv  39173  monoord2xrv  40193  sumnnodd  40342  liminfgval  40474  ioodvbdlimc2lem  40629  itgsin0pilem1  40645  stoweidlem55  40751  wallispilem1  40761  wallispilem2  40762  wallispilem4  40764  wallispi2lem1  40767  wallispi2lem2  40768  dirkerval  40787  fourierdlem2  40805  fourierdlem3  40806  fourierdlem29  40832  fourierdlem62  40864  fourierdlem80  40882  fourierdlem103  40905  fourierdlem104  40906  fourierswlem  40926  fouriersw  40927  iundjiunlem  41155  carageniuncllem2  41218  0ome  41225  hoidmv1le  41290  hoidmvlelem3  41293  smflimsuplem7  41514  issubmgm  42357  vsetrec  43017  onsetreclem1  43019  elpglem3  43027  sinhval-named  43048  coshval-named  43049  tanhval-named  43050  secval  43059  cscval  43060  cotval  43061  aacllem  43118
  Copyright terms: Public domain W3C validator