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

Theorem fvmpt 6424
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 6422 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 671 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  Vcvv 3351  cmpt 4863  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039
This theorem is referenced by:  fvmptex  6436  fvmptrabfv  6451  ofval  7053  caofinvl  7071  fvresex  7286  1stval  7317  2ndval  7318  reldm  7368  curry1val  7421  curry2val  7425  fnwelem  7443  brtpos2  7510  onovuni  7592  tz7.44-1  7655  oasuc  7758  oesuclem  7759  omsuc  7760  onasuc  7762  onmsuc  7763  fvmptmap  8046  xpcomco  8206  unxpdomlem1  8320  unfilem2  8381  ordtypelem3  8581  ixpiunwdom  8652  inf3lema  8685  noinfep  8721  cantnfval  8729  cantnflem1d  8749  cantnflem1  8750  r1sucg  8796  r0weon  9035  infxpenc2lem1  9042  fseqenlem1  9047  fseqenlem2  9048  dfac8alem  9052  ac5num  9059  acni2  9069  dfac4  9145  dfac2a  9152  dfacacn  9165  dfac12lem1  9167  ackbij1lem7  9250  ackbij2lem2  9264  ackbij2lem3  9265  cfsmolem  9294  fin23lem28  9364  fin23lem39  9374  isf32lem6  9382  isf32lem7  9383  isf32lem8  9384  fin1a2lem3  9426  itunifval  9440  itunisuc  9443  axdc2lem  9472  axdc3lem2  9475  axcclem  9481  zorn2lem1  9520  negiso  11205  infrenegsup  11208  uzval  11890  flval  12803  ceilval  12847  ceilval2  12849  monoord2  13039  seqf1olem2  13048  seqf1o  13049  seqdistr  13059  serle  13063  seqof  13065  swrdfv  13632  revval  13718  revfv  13721  wwlktovf1  13910  wwlktovfo  13911  sgnval  14036  cjval  14050  reval  14054  imval  14055  sqrtval  14185  absval  14186  limsupval  14413  limsupgval  14415  climmpt  14510  climle  14578  rlimdiv  14584  isercolllem1  14603  isercoll2  14607  caurcvg2  14616  fsumser  14669  isumadd  14706  fsumcnv  14712  fsumrev  14718  fsumshft  14719  iserabs  14754  cvgcmp  14755  cvgcmpce  14757  incexclem  14775  isumless  14784  divcnvshft  14794  supcvg  14795  harmonic  14798  trireciplem  14801  trirecip  14802  expcnv  14803  explecnv  14804  geolim  14808  geolim2  14809  geo2lim  14813  geomulcvg  14814  geoisum  14815  geoisumr  14816  geoisum1  14817  geoisum1c  14818  cvgrat  14822  mertenslem2  14824  mertens  14825  prodfdiv  14835  fprodser  14886  fprodshft  14913  fprodrev  14914  fprodcnv  14920  iprodmul  14940  bpolylem  14985  eftval  15013  efval  15016  efcvgfsum  15022  ege2le3  15026  eftlub  15045  eflegeo  15057  sinval  15058  cosval  15059  tanval  15064  eirrlem  15138  rpnnen2lem1  15149  rpnnen2lem2  15150  bitsfval  15353  bitsinv2  15373  bitsinv  15378  sadcf  15383  sadc0  15384  sadcp1  15385  smupf  15408  smup0  15409  smupp1  15410  qnumval  15652  qdenval  15653  phival  15679  crth  15690  phimullem  15691  eulerthlem2  15694  phisum  15702  odzval  15703  iserodd  15747  pcmpt  15803  prmreclem1  15827  prmreclem2  15828  prmreclem4  15830  prmreclem5  15831  prmreclem6  15832  1arithlem1  15834  1arithlem2  15835  vdwapfval  15882  vdwlem2  15893  vdwlem6  15897  vdwlem8  15899  vdwlem9  15900  ramub1lem2  15938  ramcl  15940  strfvnd  16083  topnval  16303  prdsplusgfval  16342  prdsmulrfval  16344  isacs  16519  acsfn  16527  cidfval  16544  homffval  16557  comfffval  16565  oppcval  16580  monfval  16599  oppcmon  16605  sectffval  16617  invffval  16625  isoval  16632  idfuval  16743  homafval  16886  arwval  16900  idafval  16914  coafval  16921  yonedainv  17129  pltfval  17167  lubfval  17186  lubval  17192  glbfval  17199  glbval  17205  p0val  17249  p1val  17250  oduval  17338  ipoval  17362  plusffval  17455  grpidval  17468  issubm  17555  prdspjmhm  17575  grpinvfval  17668  grpinvval  17669  grpsubfval  17672  grplactfval  17724  grplactval  17725  prdsinvlem  17732  mulgfval  17750  pwsmulg  17795  issubg  17802  cycsubgcl  17828  isnsg  17831  conjghm  17899  conjnmz  17902  cntrval  17959  cntzfval  17960  cntzval  17961  oppgval  17984  symgval  18006  psgnfval  18127  psgnval  18134  odfval  18159  odval  18160  sylow1lem4  18223  pgpssslw  18236  sylow2blem3  18244  sylow3lem2  18250  lsmfval  18260  pj1fval  18314  efgval  18337  efgsval  18351  frgpval  18378  vrgpval  18387  mulgmhm  18440  mulgghm  18441  ablfaclem1  18692  mgpval  18700  srglmhm  18743  srgrmhm  18744  ringlghm  18812  ringrghm  18813  opprval  18832  dvdsrval  18853  isunit  18865  invrfval  18881  dvrfval  18892  isirred  18907  issubrg  18990  abvfval  19028  abvtrivd  19050  staffval  19057  stafval  19058  scaffval  19091  lmodvsghm  19134  lssset  19144  lspfval  19186  islbs  19289  sraval  19391  rlmval  19406  2idlval  19448  lpival  19460  rrgval  19502  fidomndrnglem  19521  aspval  19543  asclfval  19549  asclval  19550  psrmulval  19601  psrlidm  19618  psrridm  19619  mvrval  19636  mvrval2  19637  mplmonmul  19679  evlslem3  19729  evlslem1  19730  evlsval  19734  evlssca  19737  evlsvar  19738  psr1val  19771  vr1val  19777  ply1val  19779  coe1fval  19790  coe1fv  19791  coe1tmmul2  19861  coe1tmmul  19862  coe1tmmul2fv  19863  coe1pwmulfv  19865  evls1val  19900  evl1fval  19907  evl1val  19908  expmhm  20030  expghm  20059  mulgghm2  20060  mulgrhm  20061  zrhval  20071  zrhmulg  20073  zlmval  20079  chrval  20088  znval  20098  znzrhval  20110  evpmss  20147  psgnevpmb  20148  ip0l  20198  ipffval  20210  ocvfval  20227  ocvval  20228  cssval  20243  thlval  20256  pjfval  20267  pjval  20271  isobs  20281  prdsinvgd2  20303  uvcresum  20349  frlmup1  20354  frlmup2  20355  islinds  20365  islindf5  20395  mamulid  20464  mamurid  20465  mdetleib  20611  mdetleib1  20615  mdetunilem9  20644  mdetuni0  20645  mdetmul  20647  cpmidpmatlem1  20895  ordtval  21214  cnpval  21261  ptpjpre1  21595  ptpjopn  21636  dfac14  21642  upxp  21647  uptx  21649  hauseqlcld  21670  txlm  21672  xkoptsub  21678  xkoinjcn  21711  kqval  21750  xpstopnlem1  21833  fmval  21967  flfval  22014  ptcmplem2  22077  ptcmplem3  22078  symgtgp  22125  qustgpopn  22143  ussval  22283  iscfilu  22312  ispsmet  22329  ismet  22348  isxmet  22349  mopnval  22463  prdsxmslem2  22554  nmfval  22613  nmval  22614  nmoval  22739  metdsval  22870  divcn  22891  mulc1cncf  22928  icopnfhmeo  22962  iccpnfhmeo  22964  xrhmeo  22965  cnheiborlem  22973  evth  22978  evth2  22979  lebnumlem3  22982  isphtpy  23000  isphtpc  23013  pcofval  23029  pcovalg  23031  pco1  23034  pcopt  23041  pcopt2  23042  pcoass  23043  pcorevcl  23044  pcorevlem  23045  pcorev2  23047  pi1xfrcnv  23076  cphnm  23212  tchval  23236  tchnmval  23247  cfilfval  23281  iscmet  23301  iscmet3lem3  23307  rrxval  23394  ehlval  23412  ivth2  23443  ovolval  23461  ovollb2lem  23476  ovolunlem1a  23484  ovolunlem1  23485  ovoliunlem1  23490  ovoliunlem2  23491  ovolicc1  23504  voliunlem1  23538  voliunlem2  23539  voliunlem3  23540  volsup  23544  ioorval  23562  uniioombllem3  23573  uniioombllem6  23576  volsup2  23593  volcn  23594  volivth  23595  vitalilem2  23597  vitalilem3  23598  vitalilem4  23599  vitali  23601  mbfmax  23636  mbfimaopnlem  23642  itg1val  23670  i1f1lem  23676  itg11  23678  itg1addlem4  23686  itg1mulc  23691  i1fres  23692  itg1climres  23701  mbfi1fseqlem2  23703  mbfi1fseqlem3  23704  mbfi1fseqlem6  23707  mbfi1flimlem  23709  mbfi1flim  23710  mbfmullem2  23711  itg2seq  23729  itg2uba  23730  itg2splitlem  23735  itg2monolem1  23737  itg2monolem2  23738  itg2monolem3  23739  itg2mono  23740  itg2i1fseqle  23741  itg2i1fseq  23742  itg2i1fseq2  23743  itg2addlem  23745  itg2cnlem1  23748  itg2cn  23750  limccnp2  23876  dvnff  23906  dvnp1  23908  cpnfval  23915  elcpn  23917  dvrec  23938  dvcnvlem  23959  dveflem  23962  dvef  23963  dvferm1  23968  dvferm2  23970  rolle  23973  dvlip  23976  dvlipcn  23977  dv11cn  23984  dvivthlem1  23991  dvivth  23993  lhop1lem  23996  ftc1lem1  24018  ftc1lem5  24023  ftc2  24027  itgsubstlem  24031  tdeglem3  24039  tdeglem4  24040  mdegval  24043  mdegmullem  24058  deg1fval  24060  deg1ldg  24072  deg1leb  24075  coe1mul3  24079  uc1pval  24119  mon1pval  24121  q1pval  24133  r1pval  24136  ply1remlem  24142  ig1pval  24152  plyval  24169  elply2  24172  plyeq0lem  24186  coeval  24199  dgrval  24204  coeid2  24215  coemullem  24226  coemul  24228  elqaalem1  24294  elqaalem2  24295  elqaalem3  24296  iaa  24300  aareccl  24301  aannenlem1  24303  geolim3  24314  aaliou3lem1  24317  aaliou3lem2  24318  aaliou3lem5  24322  aaliou3lem6  24323  aaliou3lem7  24324  aaliou3  24326  tayl0  24336  taylthlem1  24347  taylthlem2  24348  ulmshftlem  24363  ulmshft  24364  ulmuni  24366  ulmcau  24369  ulmdvlem1  24374  ulmdvlem3  24376  mtest  24378  mtestbdd  24379  mbfulm  24380  iblulm  24381  itgulm  24382  pserval  24384  pserval2  24385  radcnvlem1  24387  radcnvlem2  24388  dvradcnv  24395  pserulm  24396  pserdvlem2  24402  pserdv  24403  abelthlem1  24405  abelthlem3  24407  abelthlem4  24408  abelthlem5  24409  abelthlem6  24410  abelthlem7  24412  abelthlem8  24413  abelthlem9  24414  resinf1o  24503  efif1olem4  24512  eff1olem  24515  logcnlem5  24613  logtayllem  24626  logtayl  24627  logtaylsum  24628  logtayl2  24629  logccv  24630  asinval  24830  acosval  24831  atanval  24832  atantayl  24885  leibpilem2  24889  leibpi  24890  leibpisum  24891  log2cnv  24892  log2tlbnd  24893  areaval  24912  efrlim  24917  dfef2  24918  amgmlem  24937  emcllem2  24944  emcllem3  24945  emcllem4  24946  emcllem5  24947  emcllem6  24948  emcllem7  24949  zetacvg  24962  lgamgulmlem4  24979  lgamgulmlem5  24980  lgamgulm2  24983  lgamcvglem  24987  igamval  24994  lgamcvg2  25002  gamcvg2lem  25006  ftalem7  25026  basellem2  25029  basellem3  25030  basellem4  25031  basellem5  25032  basellem6  25033  basellem8  25035  basellem9  25036  chtval  25057  vmaval  25060  chpval  25069  ppival  25074  muval  25079  prmorcht  25125  sqff1o  25129  dvdsflsumcom  25135  musum  25138  muinv  25140  sgmppw  25143  fsumvma  25159  pclogsum  25161  dchrfi  25201  bposlem5  25234  bposlem7  25236  bposlem8  25237  bposlem9  25238  lgsfval  25248  lgsdir  25278  lgsdilem2  25279  lgsdi  25280  lgsne0  25281  lgsqrlem2  25293  lgsqrlem4  25295  lgseisenlem2  25322  dchrmusum2  25404  dchrvmasumlem1  25405  dchrvmasumiflem1  25411  dchrvmaeq0  25414  dchrisum0fval  25415  dchrisum0re  25423  mulog2sumlem1  25444  pntrval  25472  pntsval  25482  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  pntlem3  25519  abvcxp  25525  padicfval  25526  padicval  25527  padicabv  25540  ostth1  25543  ostth2  25547  ostth3  25548  iscgrg  25628  legval  25700  ishlg  25718  ishpg  25872  iscgra  25922  isinag  25950  isleag  25954  iseqlg  25968  ttgval  25976  elee  25995  axsegconlem1  26018  axsegconlem9  26026  axsegconlem10  26027  axpasch  26042  axlowdimlem15  26057  axlowdim  26062  axeuclidlem  26063  axcontlem2  26066  eengv  26080  vtxval  26099  iedgval  26100  vtxvalOLD  26101  iedgvalOLD  26102  vtxdgval  26599  wlknwwlksninjOLD  27023  wlknwwlksnsurOLD  27024  wlkwwlkinjOLD  27031  wlkwwlksurOLD  27032  wwlksnextinj  27043  wwlksnextsur  27044  clwwlkfv  27204  clwwlknonmpt2  27261  fusgreg2wsplem  27515  fusgreghash2wsp  27520  numclwwlk1lem2fv  27542  gidval  27706  grpoinvval  27717  bafval  27799  imsval  27880  dipfval  27897  sspval  27918  nmooval  27958  hmoval  28005  ipasslem8  28032  ipasslem9  28033  ipblnfi  28051  ubthlem2  28067  htthlem  28114  normval  28321  ocval  28479  occllem  28502  hsupval  28533  pjhfval  28595  pjhval  28596  chscllem2  28837  chscllem3  28838  hosval  28939  homval  28940  hodval  28941  hfsval  28942  hfmval  28943  brafval  29142  braval  29143  kbval  29153  eigvalval  29159  cnlnadjlem1  29266  nmopadjlei  29287  hmopidmchi  29350  strlem2  29450  hstrlem2  29458  cdj3lem2  29634  ofpreima  29805  inftmrel  30074  isinftm  30075  psgnfzto1stlem  30190  smatfval  30201  lmatval  30219  locfinreflem  30247  rmulccn  30314  xrmulc1cn  30316  xrge0iifcv  30320  xrge0iifiso  30321  xrge0iifhom  30323  xrge0iif1  30324  qqhval  30358  rrhval  30380  xrhval  30402  ddeval1  30637  ddeval0  30638  sxbrsigalem0  30673  sxbrsigalem3  30674  eulerpartlemgv  30775  rrvmbfm  30844  dstrvval  30872  coinflippv  30885  ballotlem2  30890  ballotlemfval  30891  ballotlemi  30902  ballotlemsval  30910  ballotlemrval  30919  ballotth  30939  plymulx  30965  signstfv  30980  signsvvfval  30995  derangval  31487  subfacval  31493  erdszelem3  31513  erdszelem9  31519  erdszelem10  31520  txpconn  31552  indispconn  31554  cvxpconn  31562  cvmlift2lem2  31624  cvmlift2lem3  31625  cvmlift2lem7  31629  cvmliftphtlem  31637  cvmlift3lem4  31642  snmlfval  31650  snmlval  31651  mvtval  31735  mvrsval  31740  mrsubffval  31742  mrsubcv  31745  mrsubrn  31748  elmrsubrn  31755  msubffval  31758  mvhfval  31768  mvhval  31769  mpstval  31770  msrfval  31772  mstaval  31779  mclsval  31798  mppsval  31807  sinccvglem  31904  circum  31906  divcnvlin  31956  iprodefisum  31965  iprodgam  31966  faclimlem1  31967  faclimlem2  31968  faclim  31970  iprodfac  31971  faclim2  31972  dfrdg2  32037  nosupfv  32189  findabrcl  32790  dnival  32798  bj-evalval  33359  bj-inftyexpiinv  33432  bj-inftyexpidisj  33434  curfv  33722  finixpnum  33727  poimirlem16  33758  poimir  33775  broucube  33776  mblfinlem2  33780  voliunnfl  33786  volsupnfl  33787  itg2addnclem  33793  itg2addnclem3  33795  ftc1cnnc  33816  ftc1anclem5  33821  ftc1anclem6  33822  ftc1anclem7  33823  ftc1anc  33825  ftc2nc  33826  fvopabf4g  33847  sdclem2  33870  fdc  33873  lmclim2  33886  geomcau  33887  istotbnd  33900  isbnd  33911  prdsbnd2  33926  heiborlem6  33947  heiborlem7  33948  heiborlem8  33949  rrnval  33958  rrncmslem  33963  idlval  34144  pridlval  34164  maxidlval  34170  lshpset  34787  lsatset  34799  lcvfbr  34829  lflset  34868  lflnegcl  34884  lkrfval  34896  lshpkrlem1  34919  lshpkrlem2  34920  lshpkrlem3  34921  ldualset  34934  cmtfvalN  35019  cvrfval  35077  pats  35094  llnset  35313  lplnset  35337  lvolset  35380  lineset  35546  pointsetN  35549  psubspset  35552  pmapfval  35564  pmapval  35565  paddfval  35605  pclfvalN  35697  polfvalN  35712  polvalN  35713  psubclsetN  35744  watfvalN  35800  watvalN  35801  lhpset  35803  lautset  35890  pautsetN  35906  ldilfset  35916  ldilset  35917  ltrnfset  35925  ltrnset  35926  dilfsetN  35961  dilsetN  35962  trnfsetN  35964  trnsetN  35965  trlfset  35969  trlset  35970  trlval  35971  tgrpfset  36553  tgrpset  36554  tendofset  36567  tendoset  36568  tendo02  36596  tendoi  36603  erngfset  36608  erngset  36609  erngfset-rN  36616  erngset-rN  36617  cdlemksv  36653  dvafset  36813  dvaset  36814  dvaplusgv  36819  diaffval  36840  diafval  36841  diaval  36842  dvhfset  36890  dvhset  36891  cdlemm10N  36928  docaffvalN  36931  docafvalN  36932  djaffvalN  36943  djafvalN  36944  dibffval  36950  dibfval  36951  dibval  36952  dicffval  36984  dicfval  36985  dicval  36986  dihffval  37040  dihfval  37041  dihval  37042  dochffval  37159  dochfval  37160  djhffval  37206  djhfval  37207  dochfl1  37286  lpolsetN  37292  lcfrlem8  37359  lcdfval  37398  lcdval  37399  mapdffval  37436  mapdfval  37437  mapdhval  37534  hvmapffval  37568  hvmapfval  37569  hdmap1ffval  37605  hdmap1fval  37606  hdmapffval  37636  hdmapfval  37637  hgmapffval  37695  hgmapfval  37696  isnacs  37793  mzpclval  37814  mzpsubst  37837  mzprename  37838  mzpcompact2lem  37840  eldiophb  37846  diophrw  37848  eldioph2  37851  diophin  37862  diophun  37863  diophren  37903  pell1qrval  37936  pell14qrval  37938  pell1234qrval  37940  pellfundval  37970  rmxypairf1o  38002  rmxyval  38006  mzpcong  38065  pw2f1ocnv  38130  dnnumch1  38140  dfac11  38158  hbtlem1  38219  hbtlem7  38221  elmnc  38232  dgraaval  38240  mpaaval  38247  itgoval  38257  rgspnval  38264  flcidc  38270  mendval  38279  issdrg  38293  mon1pid  38309  cytpval  38313  elcnvlem  38433  comptiunov2i  38524  dftrcl3  38538  trclfvcom  38541  cnvtrclfv  38542  cotrcltrcl  38543  trclimalb2  38544  trclfvdecomr  38546  dfrtrcl3  38551  dfrtrcl4  38556  clsk1indlem0  38865  clsk1indlem2  38866  clsk1indlem3  38867  clsk1indlem4  38868  clsk1indlem1  38869  k0004val  38974  lhe4.4ex1a  39054  addrfv  39198  subrfv  39199  mulvfv  39200  monoord2xrv  40230  sumnnodd  40380  liminfgval  40512  ioodvbdlimc2lem  40667  itgsin0pilem1  40683  stoweidlem55  40789  wallispilem1  40799  wallispilem2  40800  wallispilem4  40802  wallispi2lem1  40805  wallispi2lem2  40806  dirkerval  40825  fourierdlem2  40843  fourierdlem3  40844  fourierdlem29  40870  fourierdlem62  40902  fourierdlem80  40920  fourierdlem103  40943  fourierdlem104  40944  fourierswlem  40964  fouriersw  40965  iundjiunlem  41193  carageniuncllem2  41256  0ome  41263  hoidmv1le  41328  hoidmvlelem3  41331  smflimsuplem7  41552  issubmgm  42317  vsetrec  42977  onsetreclem1  42979  elpglem3  42987  sinhval-named  43008  coshval-named  43009  tanhval-named  43010  secval  43019  cscval  43020  cotval  43021  aacllem  43078
  Copyright terms: Public domain W3C validator