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

Theorem fvmpt 6949
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 6947 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 690 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3446  cmpt 5189  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6449  df-fun 6499  df-fv 6505
This theorem is referenced by:  fvmptex  6963  fvmptrabfv  6980  mptfvmpt  7179  fvmptopab  7412  ofval  7629  caofinvl  7648  fvresex  7893  1stval  7924  2ndval  7925  reldm  7977  curry1val  8038  curry2val  8042  fsplitfpar  8051  fnwelem  8064  brtpos2  8164  onovuni  8289  tz7.44-1  8353  oasuc  8471  oesuclem  8472  omsuc  8473  onasuc  8475  onmsuc  8476  fvmptmap  8820  xpcomco  9007  unxpdomlem1  9195  unfilem2  9256  ordtypelem3  9457  ixpiunwdom  9527  inf3lema  9561  noinfep  9597  cantnfval  9605  cantnflem1d  9625  cantnflem1  9626  ssttrcl  9652  ttrcltr  9653  ttrclselem2  9663  r1sucg  9706  r0weon  9949  infxpenc2lem1  9956  fseqenlem1  9961  fseqenlem2  9962  dfac8alem  9966  ac5num  9973  acni2  9983  dfac4  10059  dfac2a  10066  dfacacn  10078  dfac12lem1  10080  ackbij1lem7  10163  ackbij2lem2  10177  ackbij2lem3  10178  cfsmolem  10207  fin23lem28  10277  fin23lem39  10287  isf32lem6  10295  isf32lem7  10296  isf32lem8  10297  fin1a2lem3  10339  itunifval  10353  itunisuc  10356  axdc2lem  10385  axdc3lem2  10388  axcclem  10394  zorn2lem1  10433  negiso  12136  infrenegsup  12139  uzval  12766  flval  13700  ceilval  13744  ceilval2  13746  monoord2  13940  seqf1olem2  13949  seqf1o  13950  seqdistr  13960  serle  13964  seqof  13966  swrdfv  14537  revval  14649  revfv  14652  wwlktovf1  14847  wwlktovfo  14848  sgnval  14974  cjval  14988  reval  14992  imval  14993  sqrtval  15123  absval  15124  limsupval  15357  limsupgval  15359  climmpt  15454  climle  15523  rlimdiv  15531  isercolllem1  15550  isercoll2  15554  caurcvg2  15563  fsumser  15616  isumadd  15653  fsumcnv  15659  fsumrev  15665  fsumshft  15666  iserabs  15701  cvgcmp  15702  cvgcmpce  15704  incexclem  15722  isumless  15731  divcnvshft  15741  supcvg  15742  harmonic  15745  trireciplem  15748  trirecip  15749  expcnv  15750  explecnv  15751  geolim  15756  geolim2  15757  geo2lim  15761  geomulcvg  15762  geoisum  15763  geoisumr  15764  geoisum1  15765  geoisum1c  15766  cvgrat  15769  mertenslem2  15771  mertens  15772  prodfdiv  15782  fprodser  15833  fprodshft  15860  fprodrev  15861  fprodcnv  15867  iprodmul  15887  bpolylem  15932  eftval  15960  efval  15963  efcvgfsum  15969  ege2le3  15973  eftlub  15992  eflegeo  16004  sinval  16005  cosval  16006  tanval  16011  eirrlem  16087  rpnnen2lem1  16097  rpnnen2lem2  16098  bitsfval  16304  bitsinv2  16324  bitsinv  16329  sadcf  16334  sadc0  16335  sadcp1  16336  smupf  16359  smup0  16360  smupp1  16361  qnumval  16613  qdenval  16614  phival  16640  crth  16651  phimullem  16652  eulerthlem2  16655  phisum  16663  odzval  16664  iserodd  16708  pcmpt  16765  prmreclem1  16789  prmreclem2  16790  prmreclem4  16792  prmreclem5  16793  prmreclem6  16794  1arithlem1  16796  1arithlem2  16797  vdwapfval  16844  vdwlem2  16855  vdwlem6  16859  vdwlem8  16861  vdwlem9  16862  ramub1lem2  16900  ramcl  16902  prmoval  16906  strfvnd  17058  topnval  17317  prdsplusgfval  17357  prdsmulrfval  17359  isacs  17532  acsfn  17540  homffval  17571  comfffval  17579  oppcval  17594  monfval  17616  oppcmon  17622  sectffval  17634  invffval  17642  isoval  17649  idfuval  17763  homafval  17916  arwval  17930  coafval  17951  yonedainv  18171  oduval  18178  pltfval  18221  lubfval  18240  lubval  18246  glbfval  18253  glbval  18259  p0val  18317  p1val  18318  ipoval  18420  plusffval  18504  grpidval  18517  issubm  18615  prdspjmhm  18640  efmnd  18681  smndex1igid  18715  grpinvfval  18790  grpinvval  18792  grpsubfval  18795  grpsubfvalALT  18796  grplactval  18850  prdsinvlem  18857  mulgfval  18875  mulgfvalALT  18876  pwsmulg  18922  issubg  18929  isnsg  18958  cycsubmel  18994  cycsubgcl  19000  conjghm  19040  conjnmz  19043  cntrval  19100  cntzfval  19101  cntzval  19102  oppgval  19126  psgnfval  19283  psgnval  19290  odfval  19315  odval  19317  sylow1lem4  19384  pgpssslw  19397  sylow2blem3  19405  sylow3lem2  19411  lsmfval  19421  pj1fval  19477  efgval  19500  efgsval  19514  frgpval  19541  vrgpval  19550  mulgmhm  19607  mulgghm  19608  ablfaclem1  19865  mgpval  19900  srglmhm  19953  srgrmhm  19954  ringlghm  20029  ringrghm  20030  pwspjmhmmgpd  20044  pwsexpg  20045  opprval  20051  dvdsrval  20075  isunit  20087  invrfval  20103  dvrfval  20114  isirred  20129  issubrg  20225  issdrg  20264  abvfval  20280  abvtrivd  20302  staffval  20309  stafval  20310  scaffval  20343  lmodvsghm  20386  lssset  20397  lspfval  20437  islbs  20540  sraval  20640  rlmval  20663  2idlval  20706  lpival  20718  rrgval  20760  fidomndrnglem  20780  expmhm  20869  expghm  20899  mulgghm2  20900  mulgrhm  20901  zrhval  20911  zrhmulg  20913  zlmval  20919  chrval  20931  znval  20941  znzrhval  20956  evpmss  20993  psgnevpmb  20994  ip0l  21043  ipffval  21055  ocvfval  21073  ocvval  21074  cssval  21089  thlval  21102  pjfval  21115  pjval  21119  isobs  21129  prdsinvgd2  21151  uvcresum  21202  frlmup1  21207  frlmup2  21208  islinds  21218  islindf5  21248  aspval  21279  asclval  21286  psrmulval  21357  psrlidm  21375  psrridm  21376  mvrval  21393  mvrval2  21394  mplmonmul  21440  evlslem3  21493  evlslem1  21495  evlsval  21499  evlssca  21502  evlsvar  21503  psr1val  21560  vr1val  21566  ply1val  21568  coe1fval  21579  coe1fv  21580  coe1tmmul2  21650  coe1tmmul  21651  coe1tmmul2fv  21652  coe1pwmulfv  21654  evls1val  21689  evl1fval  21697  evl1val  21698  mamulid  21793  mamurid  21794  mdetleib  21939  mdetleib1  21943  mdetunilem9  21972  mdetuni0  21973  mdetmul  21975  cpmidpmatlem1  22222  ordtval  22543  cnpval  22590  ptpjpre1  22925  ptpjopn  22966  dfac14  22972  upxp  22977  uptx  22979  hauseqlcld  23000  txlm  23002  xkoptsub  23008  xkoinjcn  23041  kqval  23080  xpstopnlem1  23163  fmval  23297  flfval  23344  ptcmplem2  23407  ptcmplem3  23408  symgtgp  23460  qustgpopn  23474  ussval  23614  iscfilu  23643  ispsmet  23660  ismet  23679  isxmet  23680  mopnval  23794  prdsxmslem2  23888  nmfval  23947  nmval  23948  nmoval  24082  metdsval  24213  divcn  24234  mulc1cncf  24271  icopnfhmeo  24309  iccpnfhmeo  24311  xrhmeo  24312  cnheiborlem  24320  evth  24325  evth2  24326  lebnumlem3  24329  isphtpy  24347  isphtpc  24360  pcofval  24376  pcovalg  24378  pco1  24381  pcopt  24388  pcopt2  24389  pcoass  24390  pcorevcl  24391  pcorevlem  24392  pcorev2  24394  pi1xfrcnv  24423  cphnm  24560  tcphval  24585  tcphnmval  24596  cfilfval  24631  iscmet  24651  iscmet3lem3  24657  rrxval  24754  ehlval  24781  ivth2  24822  ovolval  24840  ovollb2lem  24855  ovolunlem1a  24863  ovolunlem1  24864  ovoliunlem1  24869  ovoliunlem2  24870  ovolicc1  24883  voliunlem1  24917  voliunlem2  24918  voliunlem3  24919  volsup  24923  ioorval  24941  uniioombllem3  24952  uniioombllem6  24955  volsup2  24972  volcn  24973  volivth  24974  vitalilem2  24976  vitalilem3  24977  vitalilem4  24978  vitali  24980  mbfmax  25016  mbfimaopnlem  25022  itg1val  25050  i1f1lem  25056  itg11  25058  itg1addlem4  25066  itg1addlem4OLD  25067  itg1mulc  25072  i1fres  25073  itg1climres  25082  mbfi1fseqlem2  25084  mbfi1fseqlem3  25085  mbfi1fseqlem6  25088  mbfi1flimlem  25090  mbfi1flim  25091  mbfmullem2  25092  itg2seq  25110  itg2uba  25111  itg2splitlem  25116  itg2monolem1  25118  itg2monolem2  25119  itg2monolem3  25120  itg2mono  25121  itg2i1fseqle  25122  itg2i1fseq  25123  itg2i1fseq2  25124  itg2addlem  25126  itg2cnlem1  25129  itg2cn  25131  limccnp2  25259  dvnff  25290  dvnp1  25292  cpnfval  25299  elcpn  25301  dvrec  25322  dvcnvlem  25343  dveflem  25346  dvef  25347  dvferm1  25352  dvferm2  25354  rolle  25357  dvlip  25360  dvlipcn  25361  dv11cn  25368  dvivthlem1  25375  dvivth  25377  lhop1lem  25380  ftc1lem1  25402  ftc1lem5  25407  ftc2  25411  itgsubstlem  25415  tdeglem3  25425  tdeglem3OLD  25426  tdeglem4  25427  tdeglem4OLD  25428  mdegval  25431  mdegmullem  25446  deg1fval  25448  deg1ldg  25460  deg1leb  25463  coe1mul3  25467  uc1pval  25507  mon1pval  25509  q1pval  25521  r1pval  25524  ply1remlem  25530  ig1pval  25540  plyval  25557  elply2  25560  plyeq0lem  25574  coeval  25587  dgrval  25592  coeid2  25603  coemullem  25614  coemul  25616  elqaalem1  25682  elqaalem2  25683  elqaalem3  25684  iaa  25688  aareccl  25689  aannenlem1  25691  geolim3  25702  aaliou3lem1  25705  aaliou3lem2  25706  aaliou3lem5  25710  aaliou3lem6  25711  aaliou3lem7  25712  aaliou3  25714  tayl0  25724  taylthlem1  25735  taylthlem2  25736  ulmshftlem  25751  ulmshft  25752  ulmuni  25754  ulmcau  25757  ulmdvlem1  25762  ulmdvlem3  25764  mtest  25766  mtestbdd  25767  mbfulm  25768  iblulm  25769  itgulm  25770  pserval  25772  pserval2  25773  radcnvlem1  25775  radcnvlem2  25776  dvradcnv  25783  pserulm  25784  pserdvlem2  25790  pserdv  25791  abelthlem1  25793  abelthlem3  25795  abelthlem4  25796  abelthlem5  25797  abelthlem6  25798  abelthlem7  25800  abelthlem8  25801  abelthlem9  25802  resinf1o  25895  efif1olem4  25904  eff1olem  25907  logcnlem5  26004  logtayllem  26017  logtayl  26018  logtaylsum  26019  logtayl2  26020  logccv  26021  asinval  26235  acosval  26236  atanval  26237  atantayl  26290  leibpilem2  26294  leibpi  26295  leibpisum  26296  log2cnv  26297  log2tlbnd  26298  areaval  26317  efrlim  26322  dfef2  26323  amgmlem  26342  emcllem2  26349  emcllem3  26350  emcllem4  26351  emcllem5  26352  emcllem6  26353  emcllem7  26354  zetacvg  26367  lgamgulmlem4  26384  lgamgulmlem5  26385  lgamgulm2  26388  lgamcvglem  26392  igamval  26399  lgamcvg2  26407  gamcvg2lem  26411  ftalem7  26431  basellem2  26434  basellem3  26435  basellem4  26436  basellem5  26437  basellem6  26438  basellem8  26440  basellem9  26441  chtval  26462  vmaval  26465  chpval  26474  ppival  26479  muval  26484  prmorcht  26530  sqff1o  26534  dvdsflsumcom  26540  musum  26543  muinv  26545  sgmppw  26548  fsumvma  26564  pclogsum  26566  dchrfi  26606  bposlem5  26639  bposlem7  26641  bposlem8  26642  bposlem9  26643  lgsfval  26653  lgsdir  26683  lgsdilem2  26684  lgsdi  26685  lgsne0  26686  lgsqrlem2  26698  lgsqrlem4  26700  lgseisenlem2  26727  dchrmusum2  26845  dchrvmasumlem1  26846  dchrvmasumiflem1  26852  dchrvmaeq0  26855  dchrisum0fval  26856  dchrisum0re  26864  mulog2sumlem1  26885  pntrval  26913  pntsval  26923  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntlem3  26960  abvcxp  26966  padicfval  26967  padicval  26968  padicabv  26981  ostth1  26984  ostth2  26988  ostth3  26989  nosupfv  27057  noinffv  27072  newval  27188  leftval  27196  rightval  27197  iscgrg  27457  legval  27529  ishpg  27704  iscgra  27754  isinag  27783  isleag  27792  iseqlg  27812  ttgval  27820  ttgvalOLD  27821  elee  27846  axsegconlem1  27869  axsegconlem9  27877  axsegconlem10  27878  axpasch  27893  axlowdimlem15  27908  axlowdim  27913  axeuclidlem  27914  axcontlem2  27917  eengv  27931  vtxval  27954  iedgval  27955  edgval  28003  vtxdgval  28419  wwlksnextinj  28847  wwlksnextsurj  28848  clwwlkfv  28995  clwwlknonmpo  29036  fusgreg2wsplem  29280  fusgreghash2wsp  29285  numclwwlk1lem2fv  29303  gidval  29457  grpoinvval  29468  bafval  29549  imsval  29630  dipfval  29647  sspval  29668  nmooval  29708  hmoval  29755  ipasslem8  29782  ipasslem9  29783  ipblnfi  29800  ubthlem2  29816  htthlem  29862  normval  30069  ocval  30225  occllem  30248  hsupval  30279  pjhfval  30341  pjhval  30342  chscllem2  30583  chscllem3  30584  hosval  30685  homval  30686  hodval  30687  hfsval  30688  hfmval  30689  brafval  30888  braval  30889  kbval  30899  eigvalval  30905  cnlnadjlem1  31012  nmopadjlei  31033  hmopidmchi  31096  strlem2  31196  hstrlem2  31204  cdj3lem2  31380  ofpreima  31584  psgnfzto1stlem  31952  evpmval  31997  altgnsg  32001  inftmrel  32019  isinftm  32020  qusker  32144  qusvscpbl  32146  qusscaval  32147  mxidlval  32233  idlsrgval  32248  dimval  32303  dimvalfi  32304  smatfval  32379  lmatval  32397  locfinreflem  32424  rspecval  32448  rmulccn  32512  xrmulc1cn  32514  xrge0iifcv  32518  xrge0iifiso  32519  xrge0iifhom  32521  xrge0iif1  32522  qqhval  32558  rrhval  32580  xrhval  32602  ddeval1  32836  ddeval0  32837  sxbrsigalem0  32874  sxbrsigalem3  32875  eulerpartlemgv  32976  rrvmbfm  33045  dstrvval  33073  coinflippv  33086  ballotlem2  33091  ballotlemfval  33092  ballotlemi  33103  ballotlemsval  33111  ballotlemrval  33120  ballotth  33140  plymulx  33163  signstfv  33178  signsvvfval  33193  derangval  33764  subfacval  33770  erdszelem3  33790  erdszelem9  33796  erdszelem10  33797  txpconn  33829  indispconn  33831  cvxpconn  33839  cvmlift2lem2  33901  cvmlift2lem3  33902  cvmlift2lem7  33906  cvmliftphtlem  33914  cvmlift3lem4  33919  snmlfval  33927  snmlval  33928  gonafv  33947  mvtval  34097  mrsubffval  34104  mrsubcv  34107  mrsubrn  34110  elmrsubrn  34117  msubffval  34120  mvhval  34131  mpstval  34132  mstaval  34141  mclsval  34160  mppsval  34169  sinccvglem  34263  circum  34265  divcnvlin  34308  iprodefisum  34317  iprodgam  34318  faclimlem1  34319  faclimlem2  34320  faclim  34322  iprodfac  34323  faclim2  34324  dfrdg2  34373  findabrcl  34929  dnival  34937  bj-evalval  35549  bj-inftyexpitaudisj  35679  bj-inftyexpiinv  35682  bj-inftyexpidisj  35684  curfv  36061  finixpnum  36066  poimirlem16  36097  poimir  36114  broucube  36115  mblfinlem2  36119  voliunnfl  36125  volsupnfl  36126  itg2addnclem  36132  itg2addnclem3  36134  ftc1cnnc  36153  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anc  36162  ftc2nc  36163  fvopabf4g  36183  sdclem2  36204  fdc  36207  lmclim2  36220  geomcau  36221  istotbnd  36231  isbnd  36242  prdsbnd2  36257  heiborlem6  36278  heiborlem7  36279  heiborlem8  36280  rrnval  36289  rrncmslem  36294  idlval  36475  pridlval  36495  maxidlval  36501  lshpset  37443  lsatset  37455  lcvfbr  37485  lflset  37524  lflnegcl  37540  lshpkrlem1  37575  lshpkrlem2  37576  lshpkrlem3  37577  ldualset  37590  cmtfvalN  37675  cvrfval  37733  pats  37750  llnset  37971  lplnset  37995  lvolset  38038  lineset  38204  pointsetN  38207  psubspset  38210  pmapval  38223  paddfval  38263  pclfvalN  38355  polfvalN  38370  polvalN  38371  psubclsetN  38402  watvalN  38459  lhpset  38461  lautset  38548  pautsetN  38564  ldilset  38575  ltrnset  38584  dilsetN  38619  trnsetN  38622  trlset  38627  trlval  38628  tgrpset  39211  tendoset  39225  tendo02  39253  erngset  39266  erngset-rN  39274  cdlemksv  39310  dvaset  39471  dvaplusgv  39476  diafval  39497  diaval  39498  dvhset  39547  cdlemm10N  39584  docafvalN  39588  djafvalN  39600  dibfval  39607  dibval  39608  dicfval  39641  dicval  39642  dihval  39698  dochfval  39816  djhfval  39863  dochfl1  39942  lpolsetN  39948  lcdval  40055  mapdhval  40190  hvmapfval  40225  hdmap1fval  40262  mhphf  40774  prjspval  40944  isnacs  41030  mzpclval  41051  mzpsubst  41074  mzprename  41075  mzpcompact2lem  41077  eldiophb  41083  diophrw  41085  eldioph2  41088  diophin  41098  diophun  41099  diophren  41139  pell1qrval  41172  pell14qrval  41174  pell1234qrval  41176  pellfundval  41206  rmxypairf1o  41238  rmxyval  41242  mzpcong  41299  pw2f1ocnv  41364  dnnumch1  41374  dfac11  41392  hbtlem1  41453  hbtlem7  41455  elmnc  41466  dgraaval  41474  mpaaval  41481  itgoval  41491  rgspnval  41498  flcidc  41504  mendval  41513  mon1pid  41535  cytpval  41539  cantnfub  41658  cantnfresb  41661  elcnvlem  41880  comptiunov2i  41985  dftrcl3  41999  trclfvcom  42002  cnvtrclfv  42003  cotrcltrcl  42004  trclimalb2  42005  trclfvdecomr  42007  dfrtrcl3  42012  dfrtrcl4  42017  clsk1indlem0  42320  clsk1indlem2  42321  clsk1indlem3  42322  clsk1indlem4  42323  clsk1indlem1  42324  k0004val  42429  lhe4.4ex1a  42616  addrfv  42756  subrfv  42757  mulvfv  42758  monoord2xrv  43726  sumnnodd  43878  liminfgval  44010  ioodvbdlimc2lem  44182  itgsin0pilem1  44198  stoweidlem55  44303  wallispilem1  44313  wallispilem2  44314  wallispilem4  44316  wallispi2lem1  44319  wallispi2lem2  44320  dirkerval  44339  fourierdlem2  44357  fourierdlem3  44358  fourierdlem29  44384  fourierdlem62  44416  fourierdlem80  44434  fourierdlem103  44457  fourierdlem104  44458  fourierswlem  44478  fouriersw  44479  iundjiunlem  44707  carageniuncllem2  44770  0ome  44777  hoidmv1le  44842  hoidmvlelem3  44845  smflimsuplem7  45074  iccpval  45614  fppr  45925  issubmgm  46090  bigoval  46642  ackval0  46773  ackval41a  46787  eenglngeehlnm  46832  prstcval  47091  mndtcval  47112  vsetrec  47155  onsetreclem1  47157  elpglem3  47165  pgindnf  47168  sinhval-named  47188  coshval-named  47189  tanhval-named  47190  secval  47199  cscval  47200  cotval  47201  aacllem  47255
  Copyright terms: Public domain W3C validator