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

Theorem fvmpt 6321
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 6319 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 707 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  Vcvv 3231  cmpt 4762  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934
This theorem is referenced by:  fvmptex  6333  fvmptrabfv  6348  ofval  6948  caofinvl  6966  fvresex  7181  1stval  7212  2ndval  7213  reldm  7263  curry1val  7315  curry2val  7319  fnwelem  7337  brtpos2  7403  onovuni  7484  tz7.44-1  7547  oasuc  7649  oesuclem  7650  omsuc  7651  onasuc  7653  onmsuc  7654  fvmptmap  7936  xpcomco  8091  unxpdomlem1  8205  unfilem2  8266  ordtypelem3  8466  ixpiunwdom  8537  inf3lema  8559  noinfep  8595  cantnfval  8603  cantnflem1d  8623  cantnflem1  8624  r1sucg  8670  r0weon  8873  infxpenc2lem1  8880  fseqenlem1  8885  fseqenlem2  8886  dfac8alem  8890  ac5num  8897  acni2  8907  dfac4  8983  dfac2a  8990  dfacacn  9001  dfac12lem1  9003  ackbij1lem7  9086  ackbij2lem2  9100  ackbij2lem3  9101  cfsmolem  9130  fin23lem28  9200  fin23lem39  9210  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  fin1a2lem3  9262  itunifval  9276  itunisuc  9279  axdc2lem  9308  axdc3lem2  9311  axcclem  9317  zorn2lem1  9356  negiso  11041  infrenegsup  11044  uzval  11727  flval  12635  ceilval  12679  ceilval2  12681  monoord2  12872  seqf1olem2  12881  seqf1o  12882  seqdistr  12892  serle  12896  seqof  12898  swrdfv  13469  revval  13555  revfv  13558  wwlktovf1  13746  wwlktovfo  13747  sgnval  13872  cjval  13886  reval  13890  imval  13891  sqrtval  14021  absval  14022  limsupval  14249  limsupgval  14251  climmpt  14346  climle  14414  rlimdiv  14420  isercolllem1  14439  isercoll2  14443  caurcvg2  14452  fsumser  14505  isumadd  14542  fsumcnv  14548  fsumrev  14555  fsumshft  14556  iserabs  14591  cvgcmp  14592  cvgcmpce  14594  incexclem  14612  isumless  14621  divcnvshft  14631  supcvg  14632  harmonic  14635  trireciplem  14638  trirecip  14639  expcnv  14640  explecnv  14641  geolim  14645  geolim2  14646  geo2lim  14650  geomulcvg  14651  geoisum  14652  geoisumr  14653  geoisum1  14654  geoisum1c  14655  cvgrat  14659  mertenslem2  14661  mertens  14662  prodfdiv  14672  fprodser  14723  fprodshft  14750  fprodrev  14751  fprodcnv  14757  iprodmul  14778  bpolylem  14823  eftval  14851  efval  14854  efcvgfsum  14860  ege2le3  14864  eftlub  14883  eflegeo  14895  sinval  14896  cosval  14897  tanval  14902  eirrlem  14976  rpnnen2lem1  14987  rpnnen2lem2  14988  bitsfval  15192  bitsinv2  15212  bitsinv  15217  sadcf  15222  sadc0  15223  sadcp1  15224  smupf  15247  smup0  15248  smupp1  15249  qnumval  15492  qdenval  15493  phival  15519  crth  15530  phimullem  15531  eulerthlem2  15534  phisum  15542  odzval  15543  iserodd  15587  pcmpt  15643  prmreclem1  15667  prmreclem2  15668  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  1arithlem1  15674  1arithlem2  15675  vdwapfval  15722  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  vdwlem9  15740  ramub1lem2  15778  ramcl  15780  strfvnd  15923  topnval  16142  prdsplusgfval  16181  prdsmulrfval  16183  isacs  16359  acsfn  16367  cidfval  16384  homffval  16397  comfffval  16405  oppcval  16420  monfval  16439  oppcmon  16445  sectffval  16457  invffval  16465  isoval  16472  idfuval  16583  homafval  16726  arwval  16740  idafval  16754  coafval  16761  yonedainv  16968  pltfval  17006  lubfval  17025  lubval  17031  glbfval  17038  glbval  17044  p0val  17088  p1val  17089  oduval  17177  ipoval  17201  plusffval  17294  grpidval  17307  issubm  17394  prdspjmhm  17414  grpinvfval  17507  grpinvval  17508  grpsubfval  17511  grplactfval  17563  grplactval  17564  prdsinvlem  17571  mulgfval  17589  pwsmulg  17634  issubg  17641  cycsubgcl  17667  isnsg  17670  conjghm  17738  conjnmz  17741  cntrval  17798  cntzfval  17799  cntzval  17800  oppgval  17823  symgval  17845  psgnfval  17966  psgnval  17973  odfval  17998  odval  17999  sylow1lem4  18062  pgpssslw  18075  sylow2blem3  18083  sylow3lem2  18089  lsmfval  18099  pj1fval  18153  efgval  18176  efgsval  18190  frgpval  18217  vrgpval  18226  mulgmhm  18279  mulgghm  18280  ablfaclem1  18530  mgpval  18538  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  opprval  18670  dvdsrval  18691  isunit  18703  invrfval  18719  dvrfval  18730  isirred  18745  issubrg  18828  abvfval  18866  abvtrivd  18888  staffval  18895  stafval  18896  scaffval  18929  lmodvsghm  18972  lssset  18982  lspfval  19021  islbs  19124  sraval  19224  rlmval  19239  2idlval  19281  lpival  19293  rrgval  19335  fidomndrnglem  19354  aspval  19376  asclfval  19382  asclval  19383  psrmulval  19434  psrlidm  19451  psrridm  19452  mvrval  19469  mvrval2  19470  mplmonmul  19512  evlslem3  19562  evlslem1  19563  evlsval  19567  evlssca  19570  evlsvar  19571  psr1val  19604  vr1val  19610  ply1val  19612  coe1fval  19623  coe1fv  19624  coe1tmmul2  19694  coe1tmmul  19695  coe1tmmul2fv  19696  coe1pwmulfv  19698  evls1val  19733  evl1fval  19740  evl1val  19741  expmhm  19863  expghm  19892  mulgghm2  19893  mulgrhm  19894  zrhval  19904  zrhmulg  19906  zlmval  19912  chrval  19921  znval  19931  znzrhval  19943  evpmss  19980  psgnevpmb  19981  ip0l  20029  ipffval  20041  ocvfval  20058  ocvval  20059  cssval  20074  thlval  20087  pjfval  20098  pjval  20102  isobs  20112  prdsinvgd2  20134  uvcresum  20180  frlmup1  20185  frlmup2  20186  islinds  20196  islindf5  20226  mamulid  20295  mamurid  20296  mdetleib  20441  mdetleib1  20445  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  cpmidpmatlem1  20723  ordtval  21041  cnpval  21088  ptpjpre1  21422  ptpjopn  21463  dfac14  21469  upxp  21474  uptx  21476  hauseqlcld  21497  txlm  21499  xkoptsub  21505  xkoinjcn  21538  kqval  21577  xpstopnlem1  21660  fmval  21794  flfval  21841  ptcmplem2  21904  ptcmplem3  21905  symgtgp  21952  qustgpopn  21970  ussval  22110  iscfilu  22139  ispsmet  22156  ismet  22175  isxmet  22176  mopnval  22290  prdsxmslem2  22381  nmfval  22440  nmval  22441  nmoval  22566  metdsval  22697  divcn  22718  mulc1cncf  22755  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  cnheiborlem  22800  evth  22805  evth2  22806  lebnumlem3  22809  isphtpy  22827  isphtpc  22840  pcofval  22856  pcovalg  22858  pco1  22861  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevcl  22871  pcorevlem  22872  pcorev2  22874  pi1xfrcnv  22903  cphnm  23039  tchval  23063  tchnmval  23074  cfilfval  23108  iscmet  23128  iscmet3lem3  23134  rrxval  23221  ehlval  23239  ivth2  23270  ovolval  23288  ovollb2lem  23302  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovolicc1  23330  voliunlem1  23364  voliunlem2  23365  voliunlem3  23366  volsup  23370  ioorval  23388  uniioombllem3  23399  uniioombllem6  23402  volsup2  23419  volcn  23420  volivth  23421  vitalilem2  23423  vitalilem3  23424  vitalilem4  23425  vitali  23427  mbfmax  23461  mbfimaopnlem  23467  itg1val  23495  i1f1lem  23501  itg11  23503  itg1addlem4  23511  itg1mulc  23516  i1fres  23517  itg1climres  23526  mbfi1fseqlem2  23528  mbfi1fseqlem3  23529  mbfi1fseqlem6  23532  mbfi1flimlem  23534  mbfi1flim  23535  mbfmullem2  23536  itg2seq  23554  itg2uba  23555  itg2splitlem  23560  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2i1fseq2  23568  itg2addlem  23570  itg2cnlem1  23573  itg2cn  23575  limccnp2  23701  dvnff  23731  dvnp1  23733  cpnfval  23740  elcpn  23742  dvrec  23763  dvcnvlem  23784  dveflem  23787  dvef  23788  dvferm1  23793  dvferm2  23795  rolle  23798  dvlip  23801  dvlipcn  23802  dv11cn  23809  dvivthlem1  23816  dvivth  23818  lhop1lem  23821  ftc1lem1  23843  ftc1lem5  23848  ftc2  23852  itgsubstlem  23856  tdeglem3  23864  tdeglem4  23865  mdegval  23868  mdegmullem  23883  deg1fval  23885  deg1ldg  23897  deg1leb  23900  coe1mul3  23904  uc1pval  23944  mon1pval  23946  q1pval  23958  r1pval  23961  ply1remlem  23967  ig1pval  23977  plyval  23994  elply2  23997  plyeq0lem  24011  coeval  24024  dgrval  24029  coeid2  24040  coemullem  24051  coemul  24053  elqaalem1  24119  elqaalem2  24120  elqaalem3  24121  iaa  24125  aareccl  24126  aannenlem1  24128  geolim3  24139  aaliou3lem1  24142  aaliou3lem2  24143  aaliou3lem5  24147  aaliou3lem6  24148  aaliou3lem7  24149  aaliou3  24151  tayl0  24161  taylthlem1  24172  taylthlem2  24173  ulmshftlem  24188  ulmshft  24189  ulmuni  24191  ulmcau  24194  ulmdvlem1  24199  ulmdvlem3  24201  mtest  24203  mtestbdd  24204  mbfulm  24205  iblulm  24206  itgulm  24207  pserval  24209  pserval2  24210  radcnvlem1  24212  radcnvlem2  24213  dvradcnv  24220  pserulm  24221  pserdvlem2  24227  pserdv  24228  abelthlem1  24230  abelthlem3  24232  abelthlem4  24233  abelthlem5  24234  abelthlem6  24235  abelthlem7  24237  abelthlem8  24238  abelthlem9  24239  resinf1o  24327  efif1olem4  24336  eff1olem  24339  logcnlem5  24437  logtayllem  24450  logtayl  24451  logtaylsum  24452  logtayl2  24453  logccv  24454  asinval  24654  acosval  24655  atanval  24656  atantayl  24709  leibpilem2  24713  leibpi  24714  leibpisum  24715  log2cnv  24716  log2tlbnd  24717  areaval  24736  efrlim  24741  dfef2  24742  amgmlem  24761  emcllem2  24768  emcllem3  24769  emcllem4  24770  emcllem5  24771  emcllem6  24772  emcllem7  24773  zetacvg  24786  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulm2  24807  lgamcvglem  24811  igamval  24818  lgamcvg2  24826  gamcvg2lem  24830  ftalem7  24850  basellem2  24853  basellem3  24854  basellem4  24855  basellem5  24856  basellem6  24857  basellem8  24859  basellem9  24860  chtval  24881  vmaval  24884  chpval  24893  ppival  24898  muval  24903  prmorcht  24949  sqff1o  24953  dvdsflsumcom  24959  musum  24962  muinv  24964  sgmppw  24967  fsumvma  24983  pclogsum  24985  dchrfi  25025  bposlem5  25058  bposlem7  25060  bposlem8  25061  bposlem9  25062  lgsfval  25072  lgsdir  25102  lgsdilem2  25103  lgsdi  25104  lgsne0  25105  lgsqrlem2  25117  lgsqrlem4  25119  lgseisenlem2  25146  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasumiflem1  25235  dchrvmaeq0  25238  dchrisum0fval  25239  dchrisum0re  25247  mulog2sumlem1  25268  pntrval  25296  pntsval  25306  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntlem3  25343  abvcxp  25349  padicfval  25350  padicval  25351  padicabv  25364  ostth1  25367  ostth2  25371  ostth3  25372  iscgrg  25452  legval  25524  ishlg  25542  ishpg  25696  iscgra  25746  isinag  25774  isleag  25778  iseqlg  25792  ttgval  25800  elee  25819  axsegconlem1  25842  axsegconlem9  25850  axsegconlem10  25851  axpasch  25866  axlowdimlem15  25881  axlowdim  25886  axeuclidlem  25887  axcontlem2  25890  eengv  25904  vtxval  25923  iedgval  25924  vtxvalOLD  25925  iedgvalOLD  25926  vtxdgval  26420  wlknwwlksninj  26843  wlknwwlksnsur  26844  wlkwwlkinj  26850  wlkwwlksur  26851  wwlksnextinj  26862  wwlksnextsur  26863  clwwlkfv  27011  clwwlknonmpt2  27062  fusgreg2wsplem  27313  fusgreghash2wsp  27318  numclwlk1lem2fv  27346  gidval  27494  grpoinvval  27505  bafval  27587  imsval  27668  dipfval  27685  sspval  27706  nmooval  27746  hmoval  27793  ipasslem8  27820  ipasslem9  27821  ipblnfi  27839  ubthlem2  27855  htthlem  27902  normval  28109  ocval  28267  occllem  28290  hsupval  28321  pjhfval  28383  pjhval  28384  chscllem2  28625  chscllem3  28626  hosval  28727  homval  28728  hodval  28729  hfsval  28730  hfmval  28731  brafval  28930  braval  28931  kbval  28941  eigvalval  28947  cnlnadjlem1  29054  nmopadjlei  29075  hmopidmchi  29138  strlem2  29238  hstrlem2  29246  cdj3lem2  29422  ofpreima  29593  inftmrel  29862  isinftm  29863  psgnfzto1stlem  29978  smatfval  29989  lmatval  30007  locfinreflem  30035  rmulccn  30102  xrmulc1cn  30104  xrge0iifcv  30108  xrge0iifiso  30109  xrge0iifhom  30111  xrge0iif1  30112  qqhval  30146  rrhval  30168  xrhval  30190  ddeval1  30425  ddeval0  30426  sxbrsigalem0  30461  sxbrsigalem3  30462  eulerpartlemgv  30563  rrvmbfm  30632  dstrvval  30660  coinflippv  30673  ballotlem2  30678  ballotlemfval  30679  ballotlemi  30690  ballotlemsval  30698  ballotlemrval  30707  ballotth  30727  plymulx  30753  signstfv  30768  signsvvfval  30783  derangval  31275  subfacval  31281  erdszelem3  31301  erdszelem9  31307  erdszelem10  31308  txpconn  31340  indispconn  31342  cvxpconn  31350  cvmlift2lem2  31412  cvmlift2lem3  31413  cvmlift2lem7  31417  cvmliftphtlem  31425  cvmlift3lem4  31430  snmlfval  31438  snmlval  31439  mvtval  31523  mvrsval  31528  mrsubffval  31530  mrsubcv  31533  mrsubrn  31536  elmrsubrn  31543  msubffval  31546  mvhfval  31556  mvhval  31557  mpstval  31558  msrfval  31560  mstaval  31567  mclsval  31586  mppsval  31595  sinccvglem  31692  circum  31694  divcnvlin  31744  iprodefisum  31753  iprodgam  31754  faclimlem1  31755  faclimlem2  31756  faclim  31758  iprodfac  31759  faclim2  31760  dfrdg2  31825  nosupfv  31977  findabrcl  32578  dnival  32586  bj-evalval  33152  bj-inftyexpiinv  33225  bj-inftyexpidisj  33227  curfv  33519  finixpnum  33524  poimirlem16  33555  poimir  33572  broucube  33573  mblfinlem2  33577  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  itg2addnclem3  33593  ftc1cnnc  33614  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anc  33623  ftc2nc  33624  fvopabf4g  33645  sdclem2  33668  fdc  33671  lmclim2  33684  geomcau  33685  istotbnd  33698  isbnd  33709  prdsbnd2  33724  heiborlem6  33745  heiborlem7  33746  heiborlem8  33747  rrnval  33756  rrncmslem  33761  idlval  33942  pridlval  33962  maxidlval  33968  lshpset  34583  lsatset  34595  lcvfbr  34625  lflset  34664  lflnegcl  34680  lkrfval  34692  lshpkrlem1  34715  lshpkrlem2  34716  lshpkrlem3  34717  ldualset  34730  cmtfvalN  34815  cvrfval  34873  pats  34890  llnset  35109  lplnset  35133  lvolset  35176  lineset  35342  pointsetN  35345  psubspset  35348  pmapfval  35360  pmapval  35361  paddfval  35401  pclfvalN  35493  polfvalN  35508  polvalN  35509  psubclsetN  35540  watfvalN  35596  watvalN  35597  lhpset  35599  lautset  35686  pautsetN  35702  ldilfset  35712  ldilset  35713  ltrnfset  35721  ltrnset  35722  dilfsetN  35757  dilsetN  35758  trnfsetN  35760  trnsetN  35761  trlfset  35765  trlset  35766  trlval  35767  tgrpfset  36349  tgrpset  36350  tendofset  36363  tendoset  36364  tendo02  36392  tendoi  36399  erngfset  36404  erngset  36405  erngfset-rN  36412  erngset-rN  36413  cdlemksv  36449  dvafset  36609  dvaset  36610  dvaplusgv  36615  diaffval  36636  diafval  36637  diaval  36638  dvhfset  36686  dvhset  36687  cdlemm10N  36724  docaffvalN  36727  docafvalN  36728  djaffvalN  36739  djafvalN  36740  dibffval  36746  dibfval  36747  dibval  36748  dicffval  36780  dicfval  36781  dicval  36782  dihffval  36836  dihfval  36837  dihval  36838  dochffval  36955  dochfval  36956  djhffval  37002  djhfval  37003  dochfl1  37082  lpolsetN  37088  lcfrlem8  37155  lcdfval  37194  lcdval  37195  mapdffval  37232  mapdfval  37233  mapdhval  37330  hvmapffval  37364  hvmapfval  37365  hdmap1ffval  37402  hdmap1fval  37403  hdmapffval  37435  hdmapfval  37436  hgmapffval  37494  hgmapfval  37495  isnacs  37584  mzpclval  37605  mzpsubst  37628  mzprename  37629  mzpcompact2lem  37631  eldiophb  37637  diophrw  37639  eldioph2  37642  diophin  37653  diophun  37654  diophren  37694  pell1qrval  37727  pell14qrval  37729  pell1234qrval  37731  pellfundval  37761  rmxypairf1o  37793  rmxyval  37797  mzpcong  37856  pw2f1ocnv  37921  dnnumch1  37931  dfac11  37949  hbtlem1  38010  hbtlem7  38012  elmnc  38023  dgraaval  38031  mpaaval  38038  itgoval  38048  rgspnval  38055  flcidc  38061  mendval  38070  issdrg  38084  mon1pid  38100  cytpval  38104  elcnvlem  38224  comptiunov2i  38315  dftrcl3  38329  trclfvcom  38332  cnvtrclfv  38333  cotrcltrcl  38334  trclimalb2  38335  trclfvdecomr  38337  dfrtrcl3  38342  dfrtrcl4  38347  clsk1indlem0  38656  clsk1indlem2  38657  clsk1indlem3  38658  clsk1indlem4  38659  clsk1indlem1  38660  k0004val  38765  lhe4.4ex1a  38845  addrfv  38990  subrfv  38991  mulvfv  38992  monoord2xrv  40027  sumnnodd  40180  liminfgval  40312  ioodvbdlimc2lem  40467  itgsin0pilem1  40483  stoweidlem55  40590  wallispilem1  40600  wallispilem2  40601  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  dirkerval  40626  fourierdlem2  40644  fourierdlem3  40645  fourierdlem29  40671  fourierdlem62  40703  fourierdlem80  40721  fourierdlem103  40744  fourierdlem104  40745  fourierswlem  40765  fouriersw  40766  iundjiunlem  40994  carageniuncllem2  41057  0ome  41064  hoidmv1le  41129  hoidmvlelem3  41132  smflimsuplem7  41353  issubmgm  42114  vsetrec  42774  onsetreclem1  42776  elpglem3  42784  sinhval-named  42805  coshval-named  42806  tanhval-named  42807  secval  42816  cscval  42817  cotval  42818  aacllem  42875
  Copyright terms: Public domain W3C validator