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

Theorem fvmpt 7016
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 7014 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 691 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  Vcvv 3480  cmpt 5225  cfv 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569
This theorem is referenced by:  fvmptex  7030  fvmptrabfv  7048  mptfvmpt  7248  fvmptopab  7487  ofval  7708  caofinvl  7729  fvresex  7984  1stval  8016  2ndval  8017  reldm  8069  curry1val  8130  curry2val  8134  fsplitfpar  8143  fnwelem  8156  brtpos2  8257  onovuni  8382  tz7.44-1  8446  oasuc  8562  oesuclem  8563  omsuc  8564  onasuc  8566  onmsuc  8567  fsetfocdm  8901  fvmptmap  8921  xpcomco  9102  unxpdomlem1  9286  unfilem2  9344  ordtypelem3  9560  ixpiunwdom  9630  inf3lema  9664  noinfep  9700  cantnfval  9708  cantnflem1d  9728  cantnflem1  9729  ssttrcl  9755  ttrcltr  9756  ttrclselem2  9766  r1sucg  9809  r0weon  10052  infxpenc2lem1  10059  fseqenlem1  10064  fseqenlem2  10065  dfac8alem  10069  ac5num  10076  acni2  10086  dfac4  10162  dfac2a  10170  dfacacn  10182  dfac12lem1  10184  ackbij1lem7  10265  ackbij2lem2  10279  ackbij2lem3  10280  cfsmolem  10310  fin23lem28  10380  fin23lem39  10390  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  fin1a2lem3  10442  itunifval  10456  itunisuc  10459  axdc2lem  10488  axdc3lem2  10491  axcclem  10497  zorn2lem1  10536  negiso  12248  infrenegsup  12251  uzval  12880  flval  13834  ceilval  13878  ceilval2  13880  monoord2  14074  seqf1olem2  14083  seqf1o  14084  seqdistr  14094  serle  14098  seqof  14100  swrdfv  14686  revval  14798  revfv  14801  wwlktovf1  14996  wwlktovfo  14997  sgnval  15127  cjval  15141  reval  15145  imval  15146  sqrtval  15276  absval  15277  limsupval  15510  limsupgval  15512  climmpt  15607  climle  15676  rlimdiv  15682  isercolllem1  15701  isercoll2  15705  caurcvg2  15714  fsumser  15766  isumadd  15803  fsumcnv  15809  fsumrev  15815  fsumshft  15816  iserabs  15851  cvgcmp  15852  cvgcmpce  15854  incexclem  15872  isumless  15881  divcnvshft  15891  supcvg  15892  harmonic  15895  trireciplem  15898  trirecip  15899  expcnv  15900  explecnv  15901  geolim  15906  geolim2  15907  geo2lim  15911  geomulcvg  15912  geoisum  15913  geoisumr  15914  geoisum1  15915  geoisum1c  15916  cvgrat  15919  mertenslem2  15921  mertens  15922  prodfdiv  15932  fprodser  15985  fprodshft  16012  fprodrev  16013  fprodcnv  16019  iprodmul  16039  bpolylem  16084  eftval  16112  efval  16115  efcvgfsum  16122  ege2le3  16126  eftlub  16145  eflegeo  16157  sinval  16158  cosval  16159  tanval  16164  eirrlem  16240  rpnnen2lem1  16250  rpnnen2lem2  16251  bitsfval  16460  bitsinv2  16480  bitsinv  16485  sadcf  16490  sadc0  16491  sadcp1  16492  smupf  16515  smup0  16516  smupp1  16517  qnumval  16774  qdenval  16775  phival  16804  crth  16815  phimullem  16816  eulerthlem2  16819  phisum  16828  odzval  16829  iserodd  16873  pcmpt  16930  prmreclem1  16954  prmreclem2  16955  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  1arithlem1  16961  1arithlem2  16962  vdwapfval  17009  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  ramub1lem2  17065  ramcl  17067  prmoval  17071  strfvnd  17222  topnval  17479  prdsplusgfval  17519  prdsmulrfval  17521  isacs  17694  acsfn  17702  homffval  17733  comfffval  17741  oppcval  17756  monfval  17776  oppcmon  17782  sectffval  17794  invffval  17802  isoval  17809  idfuval  17921  homafval  18074  arwval  18088  coafval  18109  yonedainv  18326  oduval  18333  pltfval  18376  lubfval  18395  lubval  18401  glbfval  18408  glbval  18414  p0val  18472  p1val  18473  ipoval  18575  plusffval  18659  grpidval  18674  issubmgm  18715  issubm  18816  prdspjmhm  18842  efmnd  18883  smndex1igid  18917  grpinvfval  18996  grpinvval  18998  grpsubfval  19001  grpsubfvalALT  19002  grplactval  19060  prdsinvlem  19067  mulgfval  19087  mulgfvalALT  19088  pwsmulg  19137  issubg  19144  isnsg  19173  cycsubmel  19218  cycsubgcl  19224  conjghm  19267  conjnmz  19270  cntrval  19337  cntzfval  19338  cntzval  19339  oppgval  19365  psgnfval  19518  psgnval  19525  odfval  19550  odval  19552  sylow1lem4  19619  pgpssslw  19632  sylow2blem3  19640  sylow3lem2  19646  lsmfval  19656  pj1fval  19712  efgval  19735  efgsval  19749  frgpval  19776  vrgpval  19785  mulgmhm  19845  mulgghm  19846  ablfaclem1  20105  mgpval  20140  srglmhm  20218  srgrmhm  20219  ringlghm  20309  ringrghm  20310  pwspjmhmmgpd  20325  pwsexpg  20326  opprval  20335  dvdsrval  20361  isunit  20373  invrfval  20389  dvrfval  20402  isirred  20419  issubrng  20547  issubrg  20571  rgspnval  20612  rrgval  20697  fidomndrnglem  20773  issdrg  20789  abvfval  20811  abvtrivd  20833  staffval  20842  stafval  20843  scaffval  20878  lmodvsghm  20921  lssset  20931  lspfval  20971  islbs  21075  sraval  21174  rlmval  21198  2idlval  21261  lpival  21334  expmhm  21454  expghm  21486  mulgghm2  21487  mulgrhm  21488  zrhval  21518  zrhmulg  21520  zlmval  21526  chrval  21538  znval  21550  znzrhval  21565  evpmss  21604  psgnevpmb  21605  ip0l  21654  ipffval  21666  ocvfval  21684  ocvval  21685  cssval  21700  thlval  21713  pjfval  21726  pjval  21730  isobs  21740  prdsinvgd2  21762  uvcresum  21813  frlmup1  21818  frlmup2  21819  islinds  21829  islindf5  21859  aspval  21893  asclval  21900  psrmulval  21964  psrlidm  21982  psrridm  21983  psrascl  21999  mvrval  22002  mvrval2  22003  mplmonmul  22054  evlslem3  22104  evlslem1  22106  evlsval  22110  evlssca  22113  evlsvar  22114  psdmul  22170  psdmvr  22173  psr1val  22187  vr1val  22193  ply1val  22195  coe1fval  22207  coe1fv  22208  coe1tmmul2  22279  coe1tmmul  22280  coe1tmmul2fv  22281  coe1pwmulfv  22283  evls1val  22324  evl1fval  22332  evl1val  22333  mamulid  22447  mamurid  22448  mdetleib  22593  mdetleib1  22597  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  cpmidpmatlem1  22876  ordtval  23197  cnpval  23244  ptpjpre1  23579  ptpjopn  23620  dfac14  23626  upxp  23631  uptx  23633  hauseqlcld  23654  txlm  23656  xkoptsub  23662  xkoinjcn  23695  kqval  23734  xpstopnlem1  23817  fmval  23951  flfval  23998  ptcmplem2  24061  ptcmplem3  24062  symgtgp  24114  qustgpopn  24128  ussval  24268  iscfilu  24297  ispsmet  24314  ismet  24333  isxmet  24334  mopnval  24448  prdsxmslem2  24542  nmfval  24601  nmval  24602  nmoval  24736  metdsval  24869  divcnOLD  24890  divcn  24892  mulc1cncf  24931  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  cnheiborlem  24986  evth  24991  evth2  24992  lebnumlem3  24995  isphtpy  25013  isphtpc  25026  pcofval  25043  pcovalg  25045  pco1  25048  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevcl  25058  pcorevlem  25059  pcorev2  25061  pi1xfrcnv  25090  cphnm  25227  tcphval  25252  tcphnmval  25263  cfilfval  25298  iscmet  25318  iscmet3lem3  25324  rrxval  25421  ehlval  25448  ivth2  25490  ovolval  25508  ovollb2lem  25523  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliunlem2  25538  ovolicc1  25551  voliunlem1  25585  voliunlem2  25586  voliunlem3  25587  volsup  25591  ioorval  25609  uniioombllem3  25620  uniioombllem6  25623  volsup2  25640  volcn  25641  volivth  25642  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  vitali  25648  mbfmax  25684  mbfimaopnlem  25690  itg1val  25718  i1f1lem  25724  itg11  25726  itg1addlem4  25734  itg1mulc  25739  i1fres  25740  itg1climres  25749  mbfi1fseqlem2  25751  mbfi1fseqlem3  25752  mbfi1fseqlem6  25755  mbfi1flimlem  25757  mbfi1flim  25758  mbfmullem2  25759  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  itg2cnlem1  25796  itg2cn  25798  limccnp2  25927  dvnff  25959  dvnp1  25961  cpnfval  25968  elcpn  25970  dvrec  25993  dvcnvlem  26014  dveflem  26017  dvef  26018  dvferm1  26023  dvferm2  26025  rolle  26028  dvlip  26032  dvlipcn  26033  dv11cn  26040  dvivthlem1  26047  dvivth  26049  lhop1lem  26052  ftc1lem1  26076  ftc1lem5  26081  ftc2  26085  itgsubstlem  26089  tdeglem3  26098  tdeglem4  26099  mdegval  26102  mdegmullem  26117  deg1fval  26119  deg1ldg  26131  deg1leb  26134  coe1mul3  26138  uc1pval  26179  mon1pval  26181  mon1pid  26193  q1pval  26194  r1pval  26197  ply1remlem  26204  ig1pval  26215  plyval  26232  elply2  26235  plyeq0lem  26249  coeval  26262  dgrval  26267  coeid2  26278  coemullem  26289  coemul  26291  elqaalem1  26361  elqaalem2  26362  elqaalem3  26363  iaa  26367  aareccl  26368  aannenlem1  26370  geolim3  26381  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  aaliou3  26393  tayl0  26403  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmshftlem  26432  ulmshft  26433  ulmuni  26435  ulmcau  26438  ulmdvlem1  26443  ulmdvlem3  26445  mtest  26447  mtestbdd  26448  mbfulm  26449  iblulm  26450  itgulm  26451  pserval  26453  pserval2  26454  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  pserulm  26465  pserdvlem2  26472  pserdv  26473  abelthlem1  26475  abelthlem3  26477  abelthlem4  26478  abelthlem5  26479  abelthlem6  26480  abelthlem7  26482  abelthlem8  26483  abelthlem9  26484  resinf1o  26578  efif1olem4  26587  eff1olem  26590  logcnlem5  26688  logtayllem  26701  logtayl  26702  logtaylsum  26703  logtayl2  26704  logccv  26705  asinval  26925  acosval  26926  atanval  26927  atantayl  26980  leibpilem2  26984  leibpi  26985  leibpisum  26986  log2cnv  26987  log2tlbnd  26988  areaval  27007  efrlim  27012  efrlimOLD  27013  dfef2  27014  amgmlem  27033  emcllem2  27040  emcllem3  27041  emcllem4  27042  emcllem5  27043  emcllem6  27044  emcllem7  27045  zetacvg  27058  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulm2  27079  lgamcvglem  27083  igamval  27090  lgamcvg2  27098  gamcvg2lem  27102  ftalem7  27122  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  basellem6  27129  basellem8  27131  basellem9  27132  chtval  27153  vmaval  27156  chpval  27165  ppival  27170  muval  27175  prmorcht  27221  sqff1o  27225  dvdsflsumcom  27231  musum  27234  muinv  27236  sgmppw  27241  fsumvma  27257  pclogsum  27259  dchrfi  27299  bposlem5  27332  bposlem7  27334  bposlem8  27335  bposlem9  27336  lgsfval  27346  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  lgsqrlem2  27391  lgsqrlem4  27393  lgseisenlem2  27420  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasumiflem1  27545  dchrvmaeq0  27548  dchrisum0fval  27549  dchrisum0re  27557  mulog2sumlem1  27578  pntrval  27606  pntsval  27616  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntlem3  27653  abvcxp  27659  padicfval  27660  padicval  27661  padicabv  27674  ostth1  27677  ostth2  27681  ostth3  27682  nosupfv  27751  noinffv  27766  newval  27894  leftval  27902  rightval  27903  iscgrg  28520  legval  28592  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  iseqlg  28875  ttgval  28883  ttgvalOLD  28884  elee  28909  axsegconlem1  28932  axsegconlem9  28940  axsegconlem10  28941  axpasch  28956  axlowdimlem15  28971  axlowdim  28976  axeuclidlem  28977  axcontlem2  28980  eengv  28994  vtxval  29017  iedgval  29018  edgval  29066  vtxdgval  29486  wwlksnextinj  29919  wwlksnextsurj  29920  clwwlkfv  30067  clwwlknonmpo  30108  fusgreg2wsplem  30352  fusgreghash2wsp  30357  numclwwlk1lem2fv  30375  gidval  30531  grpoinvval  30542  bafval  30623  imsval  30704  dipfval  30721  sspval  30742  nmooval  30782  hmoval  30829  ipasslem8  30856  ipasslem9  30857  ipblnfi  30874  ubthlem2  30890  htthlem  30936  normval  31143  ocval  31299  occllem  31322  hsupval  31353  pjhfval  31415  pjhval  31416  chscllem2  31657  chscllem3  31658  hosval  31759  homval  31760  hodval  31761  hfsval  31762  hfmval  31763  brafval  31962  braval  31963  kbval  31973  eigvalval  31979  cnlnadjlem1  32086  nmopadjlei  32107  hmopidmchi  32170  strlem2  32270  hstrlem2  32278  cdj3lem2  32454  ofpreima  32675  psgnfzto1stlem  33120  evpmval  33165  altgnsg  33169  inftmrel  33187  isinftm  33188  qusker  33377  qusvscpbl  33379  qusvsval  33380  mxidlval  33489  idlsrgval  33531  dimval  33651  dimvalfi  33652  smatfval  33794  lmatval  33812  locfinreflem  33839  rspecval  33863  rmulccn  33927  xrmulc1cn  33929  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  xrge0iif1  33937  qqhval  33973  rrhval  33997  xrhval  34019  ddeval1  34235  ddeval0  34236  sxbrsigalem0  34273  sxbrsigalem3  34274  eulerpartlemgv  34375  rrvmbfm  34444  dstrvval  34473  coinflippv  34486  ballotlem2  34491  ballotlemfval  34492  ballotlemi  34503  ballotlemsval  34511  ballotlemrval  34520  ballotth  34540  plymulx  34563  signstfv  34578  signsvvfval  34593  derangval  35172  subfacval  35178  erdszelem3  35198  erdszelem9  35204  erdszelem10  35205  txpconn  35237  indispconn  35239  cvxpconn  35247  cvmlift2lem2  35309  cvmlift2lem3  35310  cvmlift2lem7  35314  cvmliftphtlem  35322  cvmlift3lem4  35327  snmlfval  35335  snmlval  35336  gonafv  35355  mvtval  35505  mrsubffval  35512  mrsubcv  35515  mrsubrn  35518  elmrsubrn  35525  msubffval  35528  mvhval  35539  mpstval  35540  mstaval  35549  mclsval  35568  mppsval  35577  sinccvglem  35677  circum  35679  divcnvlin  35733  iprodefisum  35741  iprodgam  35742  faclimlem1  35743  faclimlem2  35744  faclim  35746  iprodfac  35747  faclim2  35748  dfrdg2  35796  findabrcl  36455  dnival  36472  bj-evalval  37076  bj-inftyexpitaudisj  37206  bj-inftyexpiinv  37209  bj-inftyexpidisj  37211  curfv  37607  finixpnum  37612  poimirlem16  37643  poimir  37660  broucube  37661  mblfinlem2  37665  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  itg2addnclem3  37680  ftc1cnnc  37699  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anc  37708  ftc2nc  37709  fvopabf4g  37729  sdclem2  37749  fdc  37752  lmclim2  37765  geomcau  37766  istotbnd  37776  isbnd  37787  prdsbnd2  37802  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  rrnval  37834  rrncmslem  37839  idlval  38020  pridlval  38040  maxidlval  38046  lshpset  38979  lsatset  38991  lcvfbr  39021  lflset  39060  lflnegcl  39076  lshpkrlem1  39111  lshpkrlem2  39112  lshpkrlem3  39113  ldualset  39126  cmtfvalN  39211  cvrfval  39269  pats  39286  llnset  39507  lplnset  39531  lvolset  39574  lineset  39740  pointsetN  39743  psubspset  39746  pmapval  39759  paddfval  39799  pclfvalN  39891  polfvalN  39906  polvalN  39907  psubclsetN  39938  watvalN  39995  lhpset  39997  lautset  40084  pautsetN  40100  ldilset  40111  ltrnset  40120  dilsetN  40155  trnsetN  40158  trlset  40163  trlval  40164  tgrpset  40747  tendoset  40761  tendo02  40789  erngset  40802  erngset-rN  40810  cdlemksv  40846  dvaset  41007  dvaplusgv  41012  diafval  41033  diaval  41034  dvhset  41083  cdlemm10N  41120  docafvalN  41124  djafvalN  41136  dibfval  41143  dibval  41144  dicfval  41177  dicval  41178  dihval  41234  dochfval  41352  djhfval  41399  dochfl1  41478  lpolsetN  41484  lcdval  41591  mapdhval  41726  hvmapfval  41761  hdmap1fval  41798  fimgmcyc  42544  prjspval  42613  isnacs  42715  mzpclval  42736  mzpsubst  42759  mzprename  42760  mzpcompact2lem  42762  eldiophb  42768  diophrw  42770  eldioph2  42773  diophin  42783  diophun  42784  diophren  42824  pell1qrval  42857  pell14qrval  42859  pell1234qrval  42861  pellfundval  42891  rmxypairf1o  42923  rmxyval  42927  mzpcong  42984  pw2f1ocnv  43049  dnnumch1  43056  dfac11  43074  hbtlem1  43135  hbtlem7  43137  elmnc  43148  dgraaval  43156  mpaaval  43163  itgoval  43173  flcidc  43182  mendval  43191  cytpval  43214  cantnfub  43334  cantnfresb  43337  tfsconcatrev  43361  elcnvlem  43614  comptiunov2i  43719  dftrcl3  43733  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl3  43746  dfrtrcl4  43751  clsk1indlem0  44054  clsk1indlem2  44055  clsk1indlem3  44056  clsk1indlem4  44057  clsk1indlem1  44058  k0004val  44163  lhe4.4ex1a  44348  addrfv  44488  subrfv  44489  mulvfv  44490  monoord2xrv  45494  sumnnodd  45645  liminfgval  45777  ioodvbdlimc2lem  45949  itgsin0pilem1  45965  stoweidlem55  46070  wallispilem1  46080  wallispilem2  46081  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  dirkerval  46106  fourierdlem2  46124  fourierdlem3  46125  fourierdlem29  46151  fourierdlem62  46183  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  fourierswlem  46245  fouriersw  46246  iundjiunlem  46474  carageniuncllem2  46537  0ome  46544  hoidmv1le  46609  hoidmvlelem3  46612  smflimsuplem7  46841  iccpval  47402  fppr  47713  bigoval  48470  ackval0  48601  ackval41a  48615  eenglngeehlnm  48660  prstcval  49153  mndtcval  49176  vsetrec  49222  onsetreclem1  49224  elpglem3  49232  pgindnf  49235  sinhval-named  49255  coshval-named  49256  tanhval-named  49257  secval  49266  cscval  49267  cotval  49268  aacllem  49320
  Copyright terms: Public domain W3C validator