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

Theorem fvmpt 6191
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 6189 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 703 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  Vcvv 3173  cmpt 4643  cfv 5804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812
This theorem is referenced by:  fvmptex  6203  ofval  6804  caofinvl  6822  fvresex  7032  1stval  7061  2ndval  7062  reldm  7110  curry1val  7157  curry2val  7161  fnwelem  7179  brtpos2  7245  onovuni  7326  tz7.44-1  7389  oasuc  7491  oesuclem  7492  omsuc  7493  onasuc  7495  onmsuc  7496  fvmptmap  7780  xpcomco  7935  unxpdomlem1  8049  unfilem2  8110  ordtypelem3  8308  ixpiunwdom  8379  inf3lema  8404  noinfep  8440  cantnfval  8448  cantnflem1d  8468  cantnflem1  8469  r1sucg  8515  r0weon  8718  infxpenc2lem1  8725  fseqenlem1  8730  fseqenlem2  8731  dfac8alem  8735  ac5num  8742  acni2  8752  dfac4  8828  dfac2a  8835  dfacacn  8846  dfac12lem1  8848  ackbij1lem7  8931  ackbij2lem2  8945  ackbij2lem3  8946  cfsmolem  8975  fin23lem28  9045  fin23lem39  9055  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  fin1a2lem3  9107  itunifval  9121  itunisuc  9124  axdc2lem  9153  axdc3lem2  9156  axcclem  9162  zorn2lem1  9201  negiso  10880  infrenegsup  10883  uzval  11565  flval  12457  ceilval  12501  ceilval2  12503  monoord2  12694  seqf1olem2  12703  seqf1o  12704  seqdistr  12714  serle  12718  seqof  12720  swrdfv  13276  revval  13360  revfv  13363  wwlktovf1  13548  wwlktovfo  13549  sgnval  13676  cjval  13690  reval  13694  imval  13695  sqrtval  13825  absval  13826  limsupval  14053  limsupgval  14055  climmpt  14150  climle  14218  rlimdiv  14224  isercolllem1  14243  isercoll2  14247  caurcvg2  14256  fsumser  14308  isumadd  14340  fsumcnv  14346  fsumrev  14353  fsumshft  14354  iserabs  14388  cvgcmp  14389  cvgcmpce  14391  incexclem  14407  isumless  14416  divcnvshft  14426  supcvg  14427  harmonic  14430  trireciplem  14433  trirecip  14434  expcnv  14435  explecnv  14436  geolim  14440  geolim2  14441  geo2lim  14445  geomulcvg  14446  geoisum  14447  geoisumr  14448  geoisum1  14449  geoisum1c  14450  cvgrat  14454  mertenslem2  14456  mertens  14457  prodfdiv  14467  fprodser  14518  fprodshft  14545  fprodrev  14546  fprodcnv  14552  iprodmul  14573  bpolylem  14618  eftval  14646  efval  14649  efcvgfsum  14655  ege2le3  14659  eftlub  14678  eflegeo  14690  sinval  14691  cosval  14692  tanval  14697  eirrlem  14771  rpnnen2lem1  14782  rpnnen2lem2  14783  bitsfval  14983  bitsinv2  15003  bitsinv  15008  sadcf  15013  sadc0  15014  sadcp1  15015  smupf  15038  smup0  15039  smupp1  15040  qnumval  15283  qdenval  15284  phival  15310  crth  15321  phimullem  15322  eulerthlem2  15325  phisum  15333  odzval  15334  iserodd  15378  pcmpt  15434  prmreclem1  15458  prmreclem2  15459  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  1arithlem1  15465  1arithlem2  15466  vdwapfval  15513  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  ramub1lem2  15569  ramcl  15571  strfvnd  15710  topnval  15918  prdsplusgfval  15957  prdsmulrfval  15959  isacs  16135  acsfn  16143  cidfval  16160  homffval  16173  comfffval  16181  oppcval  16196  monfval  16215  oppcmon  16221  sectffval  16233  invffval  16241  isoval  16248  idfuval  16359  homafval  16502  arwval  16516  idafval  16530  coafval  16537  yonedainv  16744  pltfval  16782  lubfval  16801  lubval  16807  glbfval  16814  glbval  16820  p0val  16864  p1val  16865  oduval  16953  ipoval  16977  plusffval  17070  grpidval  17083  issubm  17170  prdspjmhm  17190  grpinvfval  17283  grpinvval  17284  grpsubfval  17287  grplactfval  17339  grplactval  17340  prdsinvlem  17347  mulgfval  17365  pwsmulg  17410  issubg  17417  cycsubgcl  17443  isnsg  17446  conjghm  17514  conjnmz  17517  cntrval  17575  cntzfval  17576  cntzval  17577  oppgval  17600  symgval  17622  psgnfval  17743  psgnval  17750  odfval  17775  odval  17776  sylow1lem4  17839  pgpssslw  17852  sylow2blem3  17860  sylow3lem2  17866  lsmfval  17876  pj1fval  17930  efgval  17953  efgsval  17967  frgpval  17994  vrgpval  18003  mulgmhm  18056  mulgghm  18057  ablfaclem1  18307  mgpval  18315  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  opprval  18447  dvdsrval  18468  isunit  18480  invrfval  18496  dvrfval  18507  isirred  18522  issubrg  18603  abvfval  18641  abvtrivd  18663  staffval  18670  stafval  18671  scaffval  18704  lmodvsghm  18747  lssset  18755  lspfval  18794  islbs  18897  sraval  18997  rlmval  19012  2idlval  19054  lpival  19066  rrgval  19108  fidomndrnglem  19127  aspval  19149  asclfval  19155  asclval  19156  psrmulval  19207  psrlidm  19224  psrridm  19225  mvrval  19242  mvrval2  19243  mplmonmul  19285  evlslem3  19335  evlslem1  19336  evlsval  19340  evlssca  19343  evlsvar  19344  psr1val  19377  vr1val  19383  ply1val  19385  coe1fval  19396  coe1fv  19397  coe1tmmul2  19467  coe1tmmul  19468  coe1tmmul2fv  19469  coe1pwmulfv  19471  evls1val  19506  evl1fval  19513  evl1val  19514  expmhm  19634  expghm  19663  mulgghm2  19664  mulgrhm  19665  zrhval  19675  zrhmulg  19677  zlmval  19683  chrval  19692  znval  19702  znzrhval  19714  evpmss  19751  psgnevpmb  19752  ip0l  19800  ipffval  19812  ocvfval  19829  ocvval  19830  cssval  19845  thlval  19858  pjfval  19869  pjval  19873  isobs  19883  prdsinvgd2  19905  uvcresum  19951  frlmup1  19956  frlmup2  19957  islinds  19967  islindf5  19997  mamulid  20066  mamurid  20067  mdetleib  20212  mdetleib1  20216  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  cpmidpmatlem1  20494  ordtval  20803  cnpval  20850  ptpjpre1  21184  ptpjopn  21225  dfac14  21231  upxp  21236  uptx  21238  hauseqlcld  21259  txlm  21261  xkoptsub  21267  xkoinjcn  21300  kqval  21339  xpstopnlem1  21422  fmval  21557  flfval  21604  ptcmplem2  21667  ptcmplem3  21668  symgtgp  21715  qustgpopn  21733  ussval  21873  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  mopnval  22053  prdsxmslem2  22144  nmfval  22203  nmval  22204  nmoval  22329  metdsval  22458  divcn  22479  mulc1cncf  22516  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  cnheiborlem  22561  evth  22566  evth2  22567  lebnumlem3  22570  isphtpy  22588  isphtpc  22601  pcofval  22618  pcovalg  22620  pco1  22623  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevcl  22633  pcorevlem  22634  pcorev2  22636  pi1xfrcnv  22665  cphnm  22801  tchval  22825  tchnmval  22836  cfilfval  22870  iscmet  22890  iscmet3lem3  22896  rrxval  22983  ehlval  23001  ivth2  23031  ovolval  23049  ovollb2lem  23063  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolicc1  23091  voliunlem1  23125  voliunlem2  23126  voliunlem3  23127  volsup  23131  ioorval  23148  uniioombllem3  23159  uniioombllem6  23162  volsup2  23179  volcn  23180  volivth  23181  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  vitali  23188  mbfmax  23222  mbfimaopnlem  23228  itg1val  23256  i1f1lem  23262  itg11  23264  itg1addlem4  23272  itg1mulc  23277  i1fres  23278  itg1climres  23287  mbfi1fseqlem2  23289  mbfi1fseqlem3  23290  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfi1flim  23296  mbfmullem2  23297  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  itg2cnlem1  23334  itg2cn  23336  limccnp2  23462  dvnff  23492  dvnp1  23494  cpnfval  23501  elcpn  23503  dvrec  23524  dvcnvlem  23543  dveflem  23546  dvef  23547  dvferm1  23552  dvferm2  23554  rolle  23557  dvlip  23560  dvlipcn  23561  dv11cn  23568  dvivthlem1  23575  dvivth  23577  lhop1lem  23580  ftc1lem1  23602  ftc1lem5  23607  ftc2  23611  itgsubstlem  23615  tdeglem3  23623  tdeglem4  23624  mdegval  23627  mdegmullem  23642  deg1fval  23644  deg1ldg  23656  deg1leb  23659  coe1mul3  23663  uc1pval  23703  mon1pval  23705  q1pval  23717  r1pval  23720  ply1remlem  23726  ig1pval  23736  plyval  23753  elply2  23756  plyeq0lem  23770  coeval  23783  dgrval  23788  coeid2  23799  coemullem  23810  coemul  23812  elqaalem1  23878  elqaalem2  23879  elqaalem3  23880  iaa  23884  aareccl  23885  aannenlem1  23887  geolim3  23898  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  aaliou3  23910  tayl0  23920  taylthlem1  23931  taylthlem2  23932  ulmshftlem  23947  ulmshft  23948  ulmuni  23950  ulmcau  23953  ulmdvlem1  23958  ulmdvlem3  23960  mtest  23962  mtestbdd  23963  mbfulm  23964  iblulm  23965  itgulm  23966  pserval  23968  pserval2  23969  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  pserulm  23980  pserdvlem2  23986  pserdv  23987  abelthlem1  23989  abelthlem3  23991  abelthlem4  23992  abelthlem5  23993  abelthlem6  23994  abelthlem7  23996  abelthlem8  23997  abelthlem9  23998  resinf1o  24086  efif1olem4  24095  eff1olem  24098  logcnlem5  24192  logtayllem  24205  logtayl  24206  logtaylsum  24207  logtayl2  24208  logccv  24209  asinval  24409  acosval  24410  atanval  24411  atantayl  24464  leibpilem2  24468  leibpi  24469  leibpisum  24470  log2cnv  24471  log2tlbnd  24472  areaval  24491  efrlim  24496  dfef2  24497  amgmlem  24516  emcllem2  24523  emcllem3  24524  emcllem4  24525  emcllem5  24526  emcllem6  24527  emcllem7  24528  zetacvg  24541  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulm2  24562  lgamcvglem  24566  igamval  24573  lgamcvg2  24581  gamcvg2lem  24585  ftalem7  24605  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem6  24612  basellem8  24614  basellem9  24615  chtval  24636  vmaval  24639  chpval  24648  ppival  24653  muval  24658  prmorcht  24704  sqff1o  24708  dvdsflsumcom  24714  musum  24717  muinv  24719  sgmppw  24722  fsumvma  24738  pclogsum  24740  dchrfi  24780  bposlem5  24813  bposlem7  24815  bposlem8  24816  bposlem9  24817  lgsfval  24827  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  lgsqrlem2  24872  lgsqrlem4  24874  lgseisenlem2  24901  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasumiflem1  24990  dchrvmaeq0  24993  dchrisum0fval  24994  dchrisum0re  25002  mulog2sumlem1  25023  pntrval  25051  pntsval  25061  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntlem3  25098  abvcxp  25104  padicfval  25105  padicval  25106  padicabv  25119  ostth1  25122  ostth2  25126  ostth3  25127  iscgrg  25207  legval  25279  ishlg  25297  ishpg  25451  iscgra  25501  isinag  25529  isleag  25533  iseqlg  25547  ttgval  25555  elee  25574  axsegconlem1  25597  axsegconlem9  25605  axsegconlem10  25606  axpasch  25621  axlowdimlem15  25636  axlowdim  25641  axeuclidlem  25642  axcontlem2  25645  eengv  25659  vtxval  25677  iedgval  25678  wlknwwlkninj  26239  wlknwwlknsur  26240  wlkiswwlkinj  26246  wlkiswwlksur  26247  wwlkextinj  26258  wwlkextsur  26259  clwwlkfv  26323  vdgrval  26423  rusgranumwlklem3  26478  numclwwlkfvc  26604  gidval  26750  grpoinvval  26761  bafval  26843  imsval  26924  dipfval  26941  sspval  26962  nmooval  27002  hmoval  27049  ipasslem8  27076  ipasslem9  27077  ipblnfi  27095  ubthlem2  27111  htthlem  27158  normval  27365  ocval  27523  occllem  27546  hsupval  27577  pjhfval  27639  pjhval  27640  chscllem2  27881  chscllem3  27882  hosval  27983  homval  27984  hodval  27985  hfsval  27986  hfmval  27987  brafval  28186  braval  28187  kbval  28197  eigvalval  28203  cnlnadjlem1  28310  nmopadjlei  28331  hmopidmchi  28394  strlem2  28494  hstrlem2  28502  cdj3lem2  28678  ofpreima  28848  inftmrel  29065  isinftm  29066  psgnfzto1stlem  29181  smatfval  29189  lmatval  29207  locfinreflem  29235  rmulccn  29302  xrmulc1cn  29304  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  xrge0iif1  29312  qqhval  29346  rrhval  29368  xrhval  29390  ddeval1  29624  ddeval0  29625  sxbrsigalem0  29660  sxbrsigalem3  29661  eulerpartlemgv  29762  rrvmbfm  29831  dstrvval  29859  coinflippv  29872  ballotlem2  29877  ballotlemfval  29878  ballotlemi  29889  ballotlemsval  29897  ballotlemrval  29906  ballotth  29926  plymulx  29951  signstfv  29966  signsvvfval  29981  derangval  30403  subfacval  30409  erdszelem3  30429  erdszelem9  30435  erdszelem10  30436  txpcon  30468  indispcon  30470  cvxpcon  30478  cvmlift2lem2  30540  cvmlift2lem3  30541  cvmlift2lem7  30545  cvmliftphtlem  30553  cvmlift3lem4  30558  snmlfval  30566  snmlval  30567  mvtval  30651  mvrsval  30656  mrsubffval  30658  mrsubcv  30661  mrsubrn  30664  elmrsubrn  30671  msubffval  30674  mvhfval  30684  mvhval  30685  mpstval  30686  msrfval  30688  mstaval  30695  mclsval  30714  mppsval  30723  sinccvglem  30820  circum  30822  divcnvlin  30871  iprodefisum  30880  iprodgam  30881  faclimlem1  30882  faclimlem2  30883  faclim  30885  iprodfac  30886  faclim2  30887  dfrdg2  30945  findabrcl  31623  dnival  31631  bj-inftyexpiinv  32272  bj-inftyexpidisj  32274  curfv  32559  finixpnum  32564  poimirlem16  32595  poimir  32612  broucube  32613  mblfinlem2  32617  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  itg2addnclem3  32633  ftc1cnnc  32654  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663  ftc2nc  32664  fvopabf4g  32685  sdclem2  32708  fdc  32711  lmclim2  32724  geomcau  32725  istotbnd  32738  isbnd  32749  prdsbnd2  32764  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  rrnval  32796  rrncmslem  32801  idlval  32982  pridlval  33002  maxidlval  33008  lshpset  33283  lsatset  33295  lcvfbr  33325  lflset  33364  lflnegcl  33380  lkrfval  33392  lshpkrlem1  33415  lshpkrlem2  33416  lshpkrlem3  33417  ldualset  33430  cmtfvalN  33515  cvrfval  33573  pats  33590  llnset  33809  lplnset  33833  lvolset  33876  lineset  34042  pointsetN  34045  psubspset  34048  pmapfval  34060  pmapval  34061  paddfval  34101  pclfvalN  34193  polfvalN  34208  polvalN  34209  psubclsetN  34240  watfvalN  34296  watvalN  34297  lhpset  34299  lautset  34386  pautsetN  34402  ldilfset  34412  ldilset  34413  ltrnfset  34421  ltrnset  34422  dilfsetN  34457  dilsetN  34458  trnfsetN  34460  trnsetN  34461  trlfset  34465  trlset  34466  trlval  34467  tgrpfset  35050  tgrpset  35051  tendofset  35064  tendoset  35065  tendo02  35093  tendoi  35100  erngfset  35105  erngset  35106  erngfset-rN  35113  erngset-rN  35114  cdlemksv  35150  dvafset  35310  dvaset  35311  dvaplusgv  35316  diaffval  35337  diafval  35338  diaval  35339  dvhfset  35387  dvhset  35388  cdlemm10N  35425  docaffvalN  35428  docafvalN  35429  djaffvalN  35440  djafvalN  35441  dibffval  35447  dibfval  35448  dibval  35449  dicffval  35481  dicfval  35482  dicval  35483  dihffval  35537  dihfval  35538  dihval  35539  dochffval  35656  dochfval  35657  djhffval  35703  djhfval  35704  dochfl1  35783  lpolsetN  35789  lcfrlem8  35856  lcdfval  35895  lcdval  35896  mapdffval  35933  mapdfval  35934  mapdhval  36031  hvmapffval  36065  hvmapfval  36066  hdmap1ffval  36103  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapffval  36195  hgmapfval  36196  isnacs  36285  mzpclval  36306  mzpsubst  36329  mzprename  36330  mzpcompact2lem  36332  eldiophb  36338  diophrw  36340  eldioph2  36343  diophin  36354  diophun  36355  diophren  36395  pell1qrval  36428  pell14qrval  36430  pell1234qrval  36432  pellfundval  36462  rmxypairf1o  36494  rmxyval  36498  mzpcong  36557  pw2f1ocnv  36622  dnnumch1  36632  dfac11  36650  hbtlem1  36712  hbtlem7  36714  elmnc  36725  dgraaval  36733  mpaaval  36740  itgoval  36750  rgspnval  36757  flcidc  36763  mendval  36772  issdrg  36786  mon1pid  36802  cytpval  36806  elcnvlem  36926  comptiunov2i  37017  dftrcl3  37031  trclfvcom  37034  cnvtrclfv  37035  cotrcltrcl  37036  trclimalb2  37037  trclfvdecomr  37039  dfrtrcl3  37044  dfrtrcl4  37049  clsk1indlem0  37359  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  k0004val  37468  lhe4.4ex1a  37550  addrfv  37694  subrfv  37695  mulvfv  37696  sumnnodd  38697  ioodvbdlimc2lem  38824  itgsin0pilem1  38841  stoweidlem55  38948  wallispilem1  38958  wallispilem2  38959  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  dirkerval  38984  fourierdlem2  39002  fourierdlem3  39003  fourierdlem29  39029  fourierdlem62  39061  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  fourierswlem  39123  fouriersw  39124  iundjiunlem  39352  carageniuncllem2  39412  0ome  39419  hoidmv1le  39484  hoidmvlelem3  39487  vtxdgval  40684  wlknwwlksninj  41086  wlknwwlksnsur  41087  wlkwwlkinj  41093  wlkwwlksur  41094  wwlksnextinj  41105  wwlksnextsur  41106  clwwlksfv  41223  issubmgm  41579  vsetrec  42245  onsetreclem1  42247  elpglem3  42255  sinhval-named  42276  coshval-named  42277  tanhval-named  42278  secval  42287  cscval  42288  cotval  42289  aacllem  42356
  Copyright terms: Public domain W3C validator