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

Theorem fvmpt 6762
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 6760 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 687 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3495  cmpt 5138  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357
This theorem is referenced by:  fvmptex  6775  fvmptrabfv  6792  mptfvmpt  6982  ofval  7407  caofinvl  7425  fvresex  7652  1stval  7682  2ndval  7683  reldm  7734  curry1val  7791  curry2val  7795  fsplitfpar  7805  fnwelem  7816  brtpos2  7889  onovuni  7970  tz7.44-1  8033  oasuc  8140  oesuclem  8141  omsuc  8142  onasuc  8144  onmsuc  8145  fvmptmap  8435  xpcomco  8596  unxpdomlem1  8711  unfilem2  8772  ordtypelem3  8973  ixpiunwdom  9044  inf3lema  9076  noinfep  9112  cantnfval  9120  cantnflem1d  9140  cantnflem1  9141  r1sucg  9187  r0weon  9427  infxpenc2lem1  9434  fseqenlem1  9439  fseqenlem2  9440  dfac8alem  9444  ac5num  9451  acni2  9461  dfac4  9537  dfac2a  9544  dfacacn  9556  dfac12lem1  9558  ackbij1lem7  9637  ackbij2lem2  9651  ackbij2lem3  9652  cfsmolem  9681  fin23lem28  9751  fin23lem39  9761  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  fin1a2lem3  9813  itunifval  9827  itunisuc  9830  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  zorn2lem1  9907  negiso  11610  infrenegsup  11613  uzval  12234  flval  13154  ceilval  13198  ceilval2  13200  monoord2  13391  seqf1olem2  13400  seqf1o  13401  seqdistr  13411  serle  13415  seqof  13417  swrdfv  14000  revval  14112  revfv  14115  wwlktovf1  14311  wwlktovfo  14312  sgnval  14437  cjval  14451  reval  14455  imval  14456  sqrtval  14586  absval  14587  limsupval  14821  limsupgval  14823  climmpt  14918  climle  14986  rlimdiv  14992  isercolllem1  15011  isercoll2  15015  caurcvg2  15024  fsumser  15077  isumadd  15112  fsumcnv  15118  fsumrev  15124  fsumshft  15125  iserabs  15160  cvgcmp  15161  cvgcmpce  15163  incexclem  15181  isumless  15190  divcnvshft  15200  supcvg  15201  harmonic  15204  trireciplem  15207  trirecip  15208  expcnv  15209  explecnv  15210  geolim  15216  geolim2  15217  geo2lim  15221  geomulcvg  15222  geoisum  15223  geoisumr  15224  geoisum1  15225  geoisum1c  15226  cvgrat  15229  mertenslem2  15231  mertens  15232  prodfdiv  15242  fprodser  15293  fprodshft  15320  fprodrev  15321  fprodcnv  15327  iprodmul  15347  bpolylem  15392  eftval  15420  efval  15423  efcvgfsum  15429  ege2le3  15433  eftlub  15452  eflegeo  15464  sinval  15465  cosval  15466  tanval  15471  eirrlem  15547  rpnnen2lem1  15557  rpnnen2lem2  15558  bitsfval  15762  bitsinv2  15782  bitsinv  15787  sadcf  15792  sadc0  15793  sadcp1  15794  smupf  15817  smup0  15818  smupp1  15819  qnumval  16067  qdenval  16068  phival  16094  crth  16105  phimullem  16106  eulerthlem2  16109  phisum  16117  odzval  16118  iserodd  16162  pcmpt  16218  prmreclem1  16242  prmreclem2  16243  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  1arithlem1  16249  1arithlem2  16250  vdwapfval  16297  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  ramub1lem2  16353  ramcl  16355  prmoval  16359  strfvnd  16492  topnval  16698  prdsplusgfval  16737  prdsmulrfval  16739  isacs  16912  acsfn  16920  homffval  16950  comfffval  16958  oppcval  16973  monfval  16992  oppcmon  16998  sectffval  17010  invffval  17018  isoval  17025  idfuval  17136  homafval  17279  arwval  17293  coafval  17314  yonedainv  17521  pltfval  17559  lubfval  17578  lubval  17584  glbfval  17591  glbval  17597  p0val  17641  p1val  17642  oduval  17730  ipoval  17754  plusffval  17848  grpidval  17861  issubm  17958  prdspjmhm  17983  grpinvfval  18082  grpinvval  18084  grpsubfval  18087  grpsubfvalALT  18088  grplactval  18141  prdsinvlem  18148  mulgfval  18166  mulgfvalALT  18167  pwsmulg  18212  issubg  18219  isnsg  18247  cycsubmel  18283  cycsubgcl  18289  conjghm  18329  conjnmz  18332  cntrval  18389  cntzfval  18390  cntzval  18391  oppgval  18415  symgval  18437  psgnfval  18559  psgnval  18566  odfval  18591  odval  18593  sylow1lem4  18657  pgpssslw  18670  sylow2blem3  18678  sylow3lem2  18684  lsmfval  18694  pj1fval  18751  efgval  18774  efgsval  18788  frgpval  18815  vrgpval  18824  mulgmhm  18879  mulgghm  18880  ablfaclem1  19138  mgpval  19173  srglmhm  19216  srgrmhm  19217  ringlghm  19285  ringrghm  19286  opprval  19305  dvdsrval  19326  isunit  19338  invrfval  19354  dvrfval  19365  isirred  19380  issubrg  19466  issdrg  19505  abvfval  19520  abvtrivd  19542  staffval  19549  stafval  19550  scaffval  19583  lmodvsghm  19626  lssset  19636  lspfval  19676  islbs  19779  sraval  19879  rlmval  19894  2idlval  19936  lpival  19948  rrgval  19990  fidomndrnglem  20009  aspval  20032  asclval  20039  psrmulval  20096  psrlidm  20113  psrridm  20114  mvrval  20131  mvrval2  20132  mplmonmul  20175  evlslem3  20223  evlslem1  20225  evlsval  20229  evlssca  20232  evlsvar  20233  psr1val  20284  vr1val  20290  ply1val  20292  coe1fval  20303  coe1fv  20304  coe1tmmul2  20374  coe1tmmul  20375  coe1tmmul2fv  20376  coe1pwmulfv  20378  evls1val  20413  evl1fval  20421  evl1val  20422  expmhm  20544  expghm  20573  mulgghm2  20574  mulgrhm  20575  zrhval  20585  zrhmulg  20587  zlmval  20593  chrval  20602  znval  20612  znzrhval  20623  evpmss  20660  psgnevpmb  20661  ip0l  20710  ipffval  20722  ocvfval  20740  ocvval  20741  cssval  20756  thlval  20769  pjfval  20780  pjval  20784  isobs  20794  prdsinvgd2  20816  uvcresum  20867  frlmup1  20872  frlmup2  20873  islinds  20883  islindf5  20913  mamulid  20980  mamurid  20981  mdetleib  21126  mdetleib1  21130  mdetunilem9  21159  mdetuni0  21160  mdetmul  21162  cpmidpmatlem1  21408  ordtval  21727  cnpval  21774  ptpjpre1  22109  ptpjopn  22150  dfac14  22156  upxp  22161  uptx  22163  hauseqlcld  22184  txlm  22186  xkoptsub  22192  xkoinjcn  22225  kqval  22264  xpstopnlem1  22347  fmval  22481  flfval  22528  ptcmplem2  22591  ptcmplem3  22592  symgtgp  22639  qustgpopn  22657  ussval  22797  iscfilu  22826  ispsmet  22843  ismet  22862  isxmet  22863  mopnval  22977  prdsxmslem2  23068  nmfval  23127  nmval  23128  nmoval  23253  metdsval  23384  divcn  23405  mulc1cncf  23442  icopnfhmeo  23476  iccpnfhmeo  23478  xrhmeo  23479  cnheiborlem  23487  evth  23492  evth2  23493  lebnumlem3  23496  isphtpy  23514  isphtpc  23527  pcofval  23543  pcovalg  23545  pco1  23548  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevcl  23558  pcorevlem  23559  pcorev2  23561  pi1xfrcnv  23590  cphnm  23726  tcphval  23750  tcphnmval  23761  cfilfval  23796  iscmet  23816  iscmet3lem3  23822  rrxval  23919  ehlval  23946  ivth2  23985  ovolval  24003  ovollb2lem  24018  ovolunlem1a  24026  ovolunlem1  24027  ovoliunlem1  24032  ovoliunlem2  24033  ovolicc1  24046  voliunlem1  24080  voliunlem2  24081  voliunlem3  24082  volsup  24086  ioorval  24104  uniioombllem3  24115  uniioombllem6  24118  volsup2  24135  volcn  24136  volivth  24137  vitalilem2  24139  vitalilem3  24140  vitalilem4  24141  vitali  24143  mbfmax  24179  mbfimaopnlem  24185  itg1val  24213  i1f1lem  24219  itg11  24221  itg1addlem4  24229  itg1mulc  24234  i1fres  24235  itg1climres  24244  mbfi1fseqlem2  24246  mbfi1fseqlem3  24247  mbfi1fseqlem6  24250  mbfi1flimlem  24252  mbfi1flim  24253  mbfmullem2  24254  itg2seq  24272  itg2uba  24273  itg2splitlem  24278  itg2monolem1  24280  itg2monolem2  24281  itg2monolem3  24282  itg2mono  24283  itg2i1fseqle  24284  itg2i1fseq  24285  itg2i1fseq2  24286  itg2addlem  24288  itg2cnlem1  24291  itg2cn  24293  limccnp2  24419  dvnff  24449  dvnp1  24451  cpnfval  24458  elcpn  24460  dvrec  24481  dvcnvlem  24502  dveflem  24505  dvef  24506  dvferm1  24511  dvferm2  24513  rolle  24516  dvlip  24519  dvlipcn  24520  dv11cn  24527  dvivthlem1  24534  dvivth  24536  lhop1lem  24539  ftc1lem1  24561  ftc1lem5  24566  ftc2  24570  itgsubstlem  24574  tdeglem3  24582  tdeglem4  24583  mdegval  24586  mdegmullem  24601  deg1fval  24603  deg1ldg  24615  deg1leb  24618  coe1mul3  24622  uc1pval  24662  mon1pval  24664  q1pval  24676  r1pval  24679  ply1remlem  24685  ig1pval  24695  plyval  24712  elply2  24715  plyeq0lem  24729  coeval  24742  dgrval  24747  coeid2  24758  coemullem  24769  coemul  24771  elqaalem1  24837  elqaalem2  24838  elqaalem3  24839  iaa  24843  aareccl  24844  aannenlem1  24846  geolim3  24857  aaliou3lem1  24860  aaliou3lem2  24861  aaliou3lem5  24865  aaliou3lem6  24866  aaliou3lem7  24867  aaliou3  24869  tayl0  24879  taylthlem1  24890  taylthlem2  24891  ulmshftlem  24906  ulmshft  24907  ulmuni  24909  ulmcau  24912  ulmdvlem1  24917  ulmdvlem3  24919  mtest  24921  mtestbdd  24922  mbfulm  24923  iblulm  24924  itgulm  24925  pserval  24927  pserval2  24928  radcnvlem1  24930  radcnvlem2  24931  dvradcnv  24938  pserulm  24939  pserdvlem2  24945  pserdv  24946  abelthlem1  24948  abelthlem3  24950  abelthlem4  24951  abelthlem5  24952  abelthlem6  24953  abelthlem7  24955  abelthlem8  24956  abelthlem9  24957  resinf1o  25047  efif1olem4  25056  eff1olem  25059  logcnlem5  25156  logtayllem  25169  logtayl  25170  logtaylsum  25171  logtayl2  25172  logccv  25173  asinval  25387  acosval  25388  atanval  25389  atantayl  25442  leibpilem2  25447  leibpi  25448  leibpisum  25449  log2cnv  25450  log2tlbnd  25451  areaval  25470  efrlim  25475  dfef2  25476  amgmlem  25495  emcllem2  25502  emcllem3  25503  emcllem4  25504  emcllem5  25505  emcllem6  25506  emcllem7  25507  zetacvg  25520  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulm2  25541  lgamcvglem  25545  igamval  25552  lgamcvg2  25560  gamcvg2lem  25564  ftalem7  25584  basellem2  25587  basellem3  25588  basellem4  25589  basellem5  25590  basellem6  25591  basellem8  25593  basellem9  25594  chtval  25615  vmaval  25618  chpval  25627  ppival  25632  muval  25637  prmorcht  25683  sqff1o  25687  dvdsflsumcom  25693  musum  25696  muinv  25698  sgmppw  25701  fsumvma  25717  pclogsum  25719  dchrfi  25759  bposlem5  25792  bposlem7  25794  bposlem8  25795  bposlem9  25796  lgsfval  25806  lgsdir  25836  lgsdilem2  25837  lgsdi  25838  lgsne0  25839  lgsqrlem2  25851  lgsqrlem4  25853  lgseisenlem2  25880  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasumiflem1  26005  dchrvmaeq0  26008  dchrisum0fval  26009  dchrisum0re  26017  mulog2sumlem1  26038  pntrval  26066  pntsval  26076  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntlem3  26113  abvcxp  26119  padicfval  26120  padicval  26121  padicabv  26134  ostth1  26137  ostth2  26141  ostth3  26142  iscgrg  26226  legval  26298  ishpg  26473  iscgra  26523  isinag  26552  isleag  26561  iseqlg  26581  ttgval  26589  elee  26608  axsegconlem1  26631  axsegconlem9  26639  axsegconlem10  26640  axpasch  26655  axlowdimlem15  26670  axlowdim  26675  axeuclidlem  26676  axcontlem2  26679  eengv  26693  vtxval  26713  iedgval  26714  edgval  26762  vtxdgval  27178  wwlksnextinj  27605  wwlksnextsurj  27606  clwwlkfv  27755  clwwlknonmpo  27796  fusgreg2wsplem  28040  fusgreghash2wsp  28045  numclwwlk1lem2fv  28063  gidval  28217  grpoinvval  28228  bafval  28309  imsval  28390  dipfval  28407  sspval  28428  nmooval  28468  hmoval  28515  ipasslem8  28542  ipasslem9  28543  ipblnfi  28560  ubthlem2  28576  htthlem  28622  normval  28829  ocval  28985  occllem  29008  hsupval  29039  pjhfval  29101  pjhval  29102  chscllem2  29343  chscllem3  29344  hosval  29445  homval  29446  hodval  29447  hfsval  29448  hfmval  29449  brafval  29648  braval  29649  kbval  29659  eigvalval  29665  cnlnadjlem1  29772  nmopadjlei  29793  hmopidmchi  29856  strlem2  29956  hstrlem2  29964  cdj3lem2  30140  ofpreima  30339  psgnfzto1stlem  30670  evpmval  30715  altgnsg  30719  inftmrel  30737  isinftm  30738  qusker  30846  qusvscpbl  30848  qusscaval  30849  dimval  30901  dimvalfi  30902  smatfval  30960  lmatval  30978  locfinreflem  31004  rmulccn  31071  xrmulc1cn  31073  xrge0iifcv  31077  xrge0iifiso  31078  xrge0iifhom  31080  xrge0iif1  31081  qqhval  31115  rrhval  31137  xrhval  31159  ddeval1  31393  ddeval0  31394  sxbrsigalem0  31429  sxbrsigalem3  31430  eulerpartlemgv  31531  rrvmbfm  31600  dstrvval  31628  coinflippv  31641  ballotlem2  31646  ballotlemfval  31647  ballotlemi  31658  ballotlemsval  31666  ballotlemrval  31675  ballotth  31695  plymulx  31718  signstfv  31733  signsvvfval  31748  derangval  32312  subfacval  32318  erdszelem3  32338  erdszelem9  32344  erdszelem10  32345  txpconn  32377  indispconn  32379  cvxpconn  32387  cvmlift2lem2  32449  cvmlift2lem3  32450  cvmlift2lem7  32454  cvmliftphtlem  32462  cvmlift3lem4  32467  snmlfval  32475  snmlval  32476  gonafv  32495  mvtval  32645  mrsubffval  32652  mrsubcv  32655  mrsubrn  32658  elmrsubrn  32665  msubffval  32668  mvhval  32679  mpstval  32680  mstaval  32689  mclsval  32708  mppsval  32717  sinccvglem  32813  circum  32815  divcnvlin  32862  iprodefisum  32871  iprodgam  32872  faclimlem1  32873  faclimlem2  32874  faclim  32876  iprodfac  32877  faclim2  32878  dfrdg2  32938  nosupfv  33104  findabrcl  33700  dnival  33708  bj-evalval  34261  bj-inftyexpitaudisj  34380  bj-inftyexpiinv  34383  bj-inftyexpidisj  34385  curfv  34754  finixpnum  34759  poimirlem16  34790  poimir  34807  broucube  34808  mblfinlem2  34812  voliunnfl  34818  volsupnfl  34819  itg2addnclem  34825  itg2addnclem3  34827  ftc1cnnc  34848  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anc  34857  ftc2nc  34858  fvopabf4g  34879  sdclem2  34900  fdc  34903  lmclim2  34916  geomcau  34917  istotbnd  34930  isbnd  34941  prdsbnd2  34956  heiborlem6  34977  heiborlem7  34978  heiborlem8  34979  rrnval  34988  rrncmslem  34993  idlval  35174  pridlval  35194  maxidlval  35200  lshpset  35996  lsatset  36008  lcvfbr  36038  lflset  36077  lflnegcl  36093  lshpkrlem1  36128  lshpkrlem2  36129  lshpkrlem3  36130  ldualset  36143  cmtfvalN  36228  cvrfval  36286  pats  36303  llnset  36523  lplnset  36547  lvolset  36590  lineset  36756  pointsetN  36759  psubspset  36762  pmapval  36775  paddfval  36815  pclfvalN  36907  polfvalN  36922  polvalN  36923  psubclsetN  36954  watvalN  37011  lhpset  37013  lautset  37100  pautsetN  37116  ldilset  37127  ltrnset  37136  dilsetN  37171  trnsetN  37174  trlset  37179  trlval  37180  tgrpset  37763  tendoset  37777  tendo02  37805  erngset  37818  erngset-rN  37826  cdlemksv  37862  dvaset  38023  dvaplusgv  38028  diafval  38049  diaval  38050  dvhset  38099  cdlemm10N  38136  docafvalN  38140  djafvalN  38152  dibfval  38159  dibval  38160  dicfval  38193  dicval  38194  dihval  38250  dochfval  38368  djhfval  38415  dochfl1  38494  lpolsetN  38500  lcdval  38607  mapdhval  38742  hvmapfval  38777  hdmap1fval  38814  prjspval  39133  isnacs  39181  mzpclval  39202  mzpsubst  39225  mzprename  39226  mzpcompact2lem  39228  eldiophb  39234  diophrw  39236  eldioph2  39239  diophin  39249  diophun  39250  diophren  39290  pell1qrval  39323  pell14qrval  39325  pell1234qrval  39327  pellfundval  39357  rmxypairf1o  39388  rmxyval  39392  mzpcong  39449  pw2f1ocnv  39514  dnnumch1  39524  dfac11  39542  hbtlem1  39603  hbtlem7  39605  elmnc  39616  dgraaval  39624  mpaaval  39631  itgoval  39641  rgspnval  39648  flcidc  39654  mendval  39663  mon1pid  39685  cytpval  39689  elcnvlem  39841  comptiunov2i  39931  dftrcl3  39945  trclfvcom  39948  cnvtrclfv  39949  cotrcltrcl  39950  trclimalb2  39951  trclfvdecomr  39953  dfrtrcl3  39958  dfrtrcl4  39963  clsk1indlem0  40271  clsk1indlem2  40272  clsk1indlem3  40273  clsk1indlem4  40274  clsk1indlem1  40275  k0004val  40380  lhe4.4ex1a  40541  addrfv  40681  subrfv  40682  mulvfv  40683  monoord2xrv  41640  sumnnodd  41791  liminfgval  41923  ioodvbdlimc2lem  42099  itgsin0pilem1  42115  stoweidlem55  42221  wallispilem1  42231  wallispilem2  42232  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  dirkerval  42257  fourierdlem2  42275  fourierdlem3  42276  fourierdlem29  42302  fourierdlem62  42334  fourierdlem80  42352  fourierdlem103  42375  fourierdlem104  42376  fourierswlem  42396  fouriersw  42397  iundjiunlem  42622  carageniuncllem2  42685  0ome  42692  hoidmv1le  42757  hoidmvlelem3  42760  smflimsuplem7  42981  iccpval  43422  fppr  43738  issubmgm  43903  efmnd  43939  smndex1igid  43974  bigoval  44507  eenglngeehlnm  44624  vsetrec  44703  onsetreclem1  44705  elpglem3  44713  sinhval-named  44733  coshval-named  44734  tanhval-named  44735  secval  44744  cscval  44745  cotval  44746  aacllem  44800
  Copyright terms: Public domain W3C validator