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

Theorem fvmpt 6280
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 6278 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 707 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  wcel 1989  Vcvv 3198  cmpt 4727  cfv 5886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-iota 5849  df-fun 5888  df-fv 5894
This theorem is referenced by:  fvmptex  6292  ofval  6903  caofinvl  6921  fvresex  7136  1stval  7167  2ndval  7168  reldm  7216  curry1val  7267  curry2val  7271  fnwelem  7289  brtpos2  7355  onovuni  7436  tz7.44-1  7499  oasuc  7601  oesuclem  7602  omsuc  7603  onasuc  7605  onmsuc  7606  fvmptmap  7891  xpcomco  8047  unxpdomlem1  8161  unfilem2  8222  ordtypelem3  8422  ixpiunwdom  8493  inf3lema  8518  noinfep  8554  cantnfval  8562  cantnflem1d  8582  cantnflem1  8583  r1sucg  8629  r0weon  8832  infxpenc2lem1  8839  fseqenlem1  8844  fseqenlem2  8845  dfac8alem  8849  ac5num  8856  acni2  8866  dfac4  8942  dfac2a  8949  dfacacn  8960  dfac12lem1  8962  ackbij1lem7  9045  ackbij2lem2  9059  ackbij2lem3  9060  cfsmolem  9089  fin23lem28  9159  fin23lem39  9169  isf32lem6  9177  isf32lem7  9178  isf32lem8  9179  fin1a2lem3  9221  itunifval  9235  itunisuc  9238  axdc2lem  9267  axdc3lem2  9270  axcclem  9276  zorn2lem1  9315  negiso  11000  infrenegsup  11003  uzval  11686  flval  12590  ceilval  12634  ceilval2  12636  monoord2  12827  seqf1olem2  12836  seqf1o  12837  seqdistr  12847  serle  12851  seqof  12853  swrdfv  13418  revval  13503  revfv  13506  wwlktovf1  13694  wwlktovfo  13695  sgnval  13822  cjval  13836  reval  13840  imval  13841  sqrtval  13971  absval  13972  limsupval  14199  limsupgval  14201  climmpt  14296  climle  14364  rlimdiv  14370  isercolllem1  14389  isercoll2  14393  caurcvg2  14402  fsumser  14455  isumadd  14492  fsumcnv  14498  fsumrev  14505  fsumshft  14506  iserabs  14541  cvgcmp  14542  cvgcmpce  14544  incexclem  14562  isumless  14571  divcnvshft  14581  supcvg  14582  harmonic  14585  trireciplem  14588  trirecip  14589  expcnv  14590  explecnv  14591  geolim  14595  geolim2  14596  geo2lim  14600  geomulcvg  14601  geoisum  14602  geoisumr  14603  geoisum1  14604  geoisum1c  14605  cvgrat  14609  mertenslem2  14611  mertens  14612  prodfdiv  14622  fprodser  14673  fprodshft  14700  fprodrev  14701  fprodcnv  14707  iprodmul  14728  bpolylem  14773  eftval  14801  efval  14804  efcvgfsum  14810  ege2le3  14814  eftlub  14833  eflegeo  14845  sinval  14846  cosval  14847  tanval  14852  eirrlem  14926  rpnnen2lem1  14937  rpnnen2lem2  14938  bitsfval  15139  bitsinv2  15159  bitsinv  15164  sadcf  15169  sadc0  15170  sadcp1  15171  smupf  15194  smup0  15195  smupp1  15196  qnumval  15439  qdenval  15440  phival  15466  crth  15477  phimullem  15478  eulerthlem2  15481  phisum  15489  odzval  15490  iserodd  15534  pcmpt  15590  prmreclem1  15614  prmreclem2  15615  prmreclem4  15617  prmreclem5  15618  prmreclem6  15619  1arithlem1  15621  1arithlem2  15622  vdwapfval  15669  vdwlem2  15680  vdwlem6  15684  vdwlem8  15686  vdwlem9  15687  ramub1lem2  15725  ramcl  15727  strfvnd  15870  topnval  16089  prdsplusgfval  16128  prdsmulrfval  16130  isacs  16306  acsfn  16314  cidfval  16331  homffval  16344  comfffval  16352  oppcval  16367  monfval  16386  oppcmon  16392  sectffval  16404  invffval  16412  isoval  16419  idfuval  16530  homafval  16673  arwval  16687  idafval  16701  coafval  16708  yonedainv  16915  pltfval  16953  lubfval  16972  lubval  16978  glbfval  16985  glbval  16991  p0val  17035  p1val  17036  oduval  17124  ipoval  17148  plusffval  17241  grpidval  17254  issubm  17341  prdspjmhm  17361  grpinvfval  17454  grpinvval  17455  grpsubfval  17458  grplactfval  17510  grplactval  17511  prdsinvlem  17518  mulgfval  17536  pwsmulg  17581  issubg  17588  cycsubgcl  17614  isnsg  17617  conjghm  17685  conjnmz  17688  cntrval  17746  cntzfval  17747  cntzval  17748  oppgval  17771  symgval  17793  psgnfval  17914  psgnval  17921  odfval  17946  odval  17947  sylow1lem4  18010  pgpssslw  18023  sylow2blem3  18031  sylow3lem2  18037  lsmfval  18047  pj1fval  18101  efgval  18124  efgsval  18138  frgpval  18165  vrgpval  18174  mulgmhm  18227  mulgghm  18228  ablfaclem1  18478  mgpval  18486  srglmhm  18529  srgrmhm  18530  ringlghm  18598  ringrghm  18599  opprval  18618  dvdsrval  18639  isunit  18651  invrfval  18667  dvrfval  18678  isirred  18693  issubrg  18774  abvfval  18812  abvtrivd  18834  staffval  18841  stafval  18842  scaffval  18875  lmodvsghm  18918  lssset  18928  lspfval  18967  islbs  19070  sraval  19170  rlmval  19185  2idlval  19227  lpival  19239  rrgval  19281  fidomndrnglem  19300  aspval  19322  asclfval  19328  asclval  19329  psrmulval  19380  psrlidm  19397  psrridm  19398  mvrval  19415  mvrval2  19416  mplmonmul  19458  evlslem3  19508  evlslem1  19509  evlsval  19513  evlssca  19516  evlsvar  19517  psr1val  19550  vr1val  19556  ply1val  19558  coe1fval  19569  coe1fv  19570  coe1tmmul2  19640  coe1tmmul  19641  coe1tmmul2fv  19642  coe1pwmulfv  19644  evls1val  19679  evl1fval  19686  evl1val  19687  expmhm  19809  expghm  19838  mulgghm2  19839  mulgrhm  19840  zrhval  19850  zrhmulg  19852  zlmval  19858  chrval  19867  znval  19877  znzrhval  19889  evpmss  19926  psgnevpmb  19927  ip0l  19975  ipffval  19987  ocvfval  20004  ocvval  20005  cssval  20020  thlval  20033  pjfval  20044  pjval  20048  isobs  20058  prdsinvgd2  20080  uvcresum  20126  frlmup1  20131  frlmup2  20132  islinds  20142  islindf5  20172  mamulid  20241  mamurid  20242  mdetleib  20387  mdetleib1  20391  mdetunilem9  20420  mdetuni0  20421  mdetmul  20423  cpmidpmatlem1  20669  ordtval  20987  cnpval  21034  ptpjpre1  21368  ptpjopn  21409  dfac14  21415  upxp  21420  uptx  21422  hauseqlcld  21443  txlm  21445  xkoptsub  21451  xkoinjcn  21484  kqval  21523  xpstopnlem1  21606  fmval  21741  flfval  21788  ptcmplem2  21851  ptcmplem3  21852  symgtgp  21899  qustgpopn  21917  ussval  22057  iscfilu  22086  ispsmet  22103  ismet  22122  isxmet  22123  mopnval  22237  prdsxmslem2  22328  nmfval  22387  nmval  22388  nmoval  22513  metdsval  22644  divcn  22665  mulc1cncf  22702  icopnfhmeo  22736  iccpnfhmeo  22738  xrhmeo  22739  cnheiborlem  22747  evth  22752  evth2  22753  lebnumlem3  22756  isphtpy  22774  isphtpc  22787  pcofval  22804  pcovalg  22806  pco1  22809  pcopt  22816  pcopt2  22817  pcoass  22818  pcorevcl  22819  pcorevlem  22820  pcorev2  22822  pi1xfrcnv  22851  cphnm  22987  tchval  23011  tchnmval  23022  cfilfval  23056  iscmet  23076  iscmet3lem3  23082  rrxval  23169  ehlval  23187  ivth2  23218  ovolval  23236  ovollb2lem  23250  ovolunlem1a  23258  ovolunlem1  23259  ovoliunlem1  23264  ovoliunlem2  23265  ovolicc1  23278  voliunlem1  23312  voliunlem2  23313  voliunlem3  23314  volsup  23318  ioorval  23336  uniioombllem3  23347  uniioombllem6  23350  volsup2  23367  volcn  23368  volivth  23369  vitalilem2  23372  vitalilem3  23373  vitalilem4  23374  vitali  23376  mbfmax  23410  mbfimaopnlem  23416  itg1val  23444  i1f1lem  23450  itg11  23452  itg1addlem4  23460  itg1mulc  23465  i1fres  23466  itg1climres  23475  mbfi1fseqlem2  23477  mbfi1fseqlem3  23478  mbfi1fseqlem6  23481  mbfi1flimlem  23483  mbfi1flim  23484  mbfmullem2  23485  itg2seq  23503  itg2uba  23504  itg2splitlem  23509  itg2monolem1  23511  itg2monolem2  23512  itg2monolem3  23513  itg2mono  23514  itg2i1fseqle  23515  itg2i1fseq  23516  itg2i1fseq2  23517  itg2addlem  23519  itg2cnlem1  23522  itg2cn  23524  limccnp2  23650  dvnff  23680  dvnp1  23682  cpnfval  23689  elcpn  23691  dvrec  23712  dvcnvlem  23733  dveflem  23736  dvef  23737  dvferm1  23742  dvferm2  23744  rolle  23747  dvlip  23750  dvlipcn  23751  dv11cn  23758  dvivthlem1  23765  dvivth  23767  lhop1lem  23770  ftc1lem1  23792  ftc1lem5  23797  ftc2  23801  itgsubstlem  23805  tdeglem3  23813  tdeglem4  23814  mdegval  23817  mdegmullem  23832  deg1fval  23834  deg1ldg  23846  deg1leb  23849  coe1mul3  23853  uc1pval  23893  mon1pval  23895  q1pval  23907  r1pval  23910  ply1remlem  23916  ig1pval  23926  plyval  23943  elply2  23946  plyeq0lem  23960  coeval  23973  dgrval  23978  coeid2  23989  coemullem  24000  coemul  24002  elqaalem1  24068  elqaalem2  24069  elqaalem3  24070  iaa  24074  aareccl  24075  aannenlem1  24077  geolim3  24088  aaliou3lem1  24091  aaliou3lem2  24092  aaliou3lem5  24096  aaliou3lem6  24097  aaliou3lem7  24098  aaliou3  24100  tayl0  24110  taylthlem1  24121  taylthlem2  24122  ulmshftlem  24137  ulmshft  24138  ulmuni  24140  ulmcau  24143  ulmdvlem1  24148  ulmdvlem3  24150  mtest  24152  mtestbdd  24153  mbfulm  24154  iblulm  24155  itgulm  24156  pserval  24158  pserval2  24159  radcnvlem1  24161  radcnvlem2  24162  dvradcnv  24169  pserulm  24170  pserdvlem2  24176  pserdv  24177  abelthlem1  24179  abelthlem3  24181  abelthlem4  24182  abelthlem5  24183  abelthlem6  24184  abelthlem7  24186  abelthlem8  24187  abelthlem9  24188  resinf1o  24276  efif1olem4  24285  eff1olem  24288  logcnlem5  24386  logtayllem  24399  logtayl  24400  logtaylsum  24401  logtayl2  24402  logccv  24403  asinval  24603  acosval  24604  atanval  24605  atantayl  24658  leibpilem2  24662  leibpi  24663  leibpisum  24664  log2cnv  24665  log2tlbnd  24666  areaval  24685  efrlim  24690  dfef2  24691  amgmlem  24710  emcllem2  24717  emcllem3  24718  emcllem4  24719  emcllem5  24720  emcllem6  24721  emcllem7  24722  zetacvg  24735  lgamgulmlem4  24752  lgamgulmlem5  24753  lgamgulm2  24756  lgamcvglem  24760  igamval  24767  lgamcvg2  24775  gamcvg2lem  24779  ftalem7  24799  basellem2  24802  basellem3  24803  basellem4  24804  basellem5  24805  basellem6  24806  basellem8  24808  basellem9  24809  chtval  24830  vmaval  24833  chpval  24842  ppival  24847  muval  24852  prmorcht  24898  sqff1o  24902  dvdsflsumcom  24908  musum  24911  muinv  24913  sgmppw  24916  fsumvma  24932  pclogsum  24934  dchrfi  24974  bposlem5  25007  bposlem7  25009  bposlem8  25010  bposlem9  25011  lgsfval  25021  lgsdir  25051  lgsdilem2  25052  lgsdi  25053  lgsne0  25054  lgsqrlem2  25066  lgsqrlem4  25068  lgseisenlem2  25095  dchrmusum2  25177  dchrvmasumlem1  25178  dchrvmasumiflem1  25184  dchrvmaeq0  25187  dchrisum0fval  25188  dchrisum0re  25196  mulog2sumlem1  25217  pntrval  25245  pntsval  25255  pntrlog2bndlem4  25263  pntrlog2bndlem5  25264  pntlem3  25292  abvcxp  25298  padicfval  25299  padicval  25300  padicabv  25313  ostth1  25316  ostth2  25320  ostth3  25321  iscgrg  25401  legval  25473  ishlg  25491  ishpg  25645  iscgra  25695  isinag  25723  isleag  25727  iseqlg  25741  ttgval  25749  elee  25768  axsegconlem1  25791  axsegconlem9  25799  axsegconlem10  25800  axpasch  25815  axlowdimlem15  25830  axlowdim  25835  axeuclidlem  25836  axcontlem2  25839  eengv  25853  vtxval  25872  iedgval  25873  vtxvalOLD  25874  iedgvalOLD  25875  vtxdgval  26358  wlknwwlksninj  26769  wlknwwlksnsur  26770  wlkwwlkinj  26776  wlkwwlksur  26777  wwlksnextinj  26788  wwlksnextsur  26789  clwwlksfv  26909  fusgreg2wsplem  27184  fusgreghash2wsp  27189  gidval  27350  grpoinvval  27361  bafval  27443  imsval  27524  dipfval  27541  sspval  27562  nmooval  27602  hmoval  27649  ipasslem8  27676  ipasslem9  27677  ipblnfi  27695  ubthlem2  27711  htthlem  27758  normval  27965  ocval  28123  occllem  28146  hsupval  28177  pjhfval  28239  pjhval  28240  chscllem2  28481  chscllem3  28482  hosval  28583  homval  28584  hodval  28585  hfsval  28586  hfmval  28587  brafval  28786  braval  28787  kbval  28797  eigvalval  28803  cnlnadjlem1  28910  nmopadjlei  28931  hmopidmchi  28994  strlem2  29094  hstrlem2  29102  cdj3lem2  29278  ofpreima  29450  inftmrel  29719  isinftm  29720  psgnfzto1stlem  29835  smatfval  29846  lmatval  29864  locfinreflem  29892  rmulccn  29959  xrmulc1cn  29961  xrge0iifcv  29965  xrge0iifiso  29966  xrge0iifhom  29968  xrge0iif1  29969  qqhval  30003  rrhval  30025  xrhval  30047  ddeval1  30282  ddeval0  30283  sxbrsigalem0  30318  sxbrsigalem3  30319  eulerpartlemgv  30420  rrvmbfm  30489  dstrvval  30517  coinflippv  30530  ballotlem2  30535  ballotlemfval  30536  ballotlemi  30547  ballotlemsval  30555  ballotlemrval  30564  ballotth  30584  plymulx  30610  signstfv  30625  signsvvfval  30640  derangval  31134  subfacval  31140  erdszelem3  31160  erdszelem9  31166  erdszelem10  31167  txpconn  31199  indispconn  31201  cvxpconn  31209  cvmlift2lem2  31271  cvmlift2lem3  31272  cvmlift2lem7  31276  cvmliftphtlem  31284  cvmlift3lem4  31289  snmlfval  31297  snmlval  31298  mvtval  31382  mvrsval  31387  mrsubffval  31389  mrsubcv  31392  mrsubrn  31395  elmrsubrn  31402  msubffval  31405  mvhfval  31415  mvhval  31416  mpstval  31417  msrfval  31419  mstaval  31426  mclsval  31445  mppsval  31454  sinccvglem  31551  circum  31553  divcnvlin  31604  iprodefisum  31613  iprodgam  31614  faclimlem1  31615  faclimlem2  31616  faclim  31618  iprodfac  31619  faclim2  31620  dfrdg2  31685  nosupfv  31836  findabrcl  32437  dnival  32445  bj-evalval  33011  bj-inftyexpiinv  33075  bj-inftyexpidisj  33077  curfv  33369  finixpnum  33374  poimirlem16  33405  poimir  33422  broucube  33423  mblfinlem2  33427  voliunnfl  33433  volsupnfl  33434  itg2addnclem  33441  itg2addnclem3  33443  ftc1cnnc  33464  ftc1anclem5  33469  ftc1anclem6  33470  ftc1anclem7  33471  ftc1anc  33473  ftc2nc  33474  fvopabf4g  33495  sdclem2  33518  fdc  33521  lmclim2  33534  geomcau  33535  istotbnd  33548  isbnd  33559  prdsbnd2  33574  heiborlem6  33595  heiborlem7  33596  heiborlem8  33597  rrnval  33606  rrncmslem  33611  idlval  33792  pridlval  33812  maxidlval  33818  lshpset  34091  lsatset  34103  lcvfbr  34133  lflset  34172  lflnegcl  34188  lkrfval  34200  lshpkrlem1  34223  lshpkrlem2  34224  lshpkrlem3  34225  ldualset  34238  cmtfvalN  34323  cvrfval  34381  pats  34398  llnset  34617  lplnset  34641  lvolset  34684  lineset  34850  pointsetN  34853  psubspset  34856  pmapfval  34868  pmapval  34869  paddfval  34909  pclfvalN  35001  polfvalN  35016  polvalN  35017  psubclsetN  35048  watfvalN  35104  watvalN  35105  lhpset  35107  lautset  35194  pautsetN  35210  ldilfset  35220  ldilset  35221  ltrnfset  35229  ltrnset  35230  dilfsetN  35265  dilsetN  35266  trnfsetN  35268  trnsetN  35269  trlfset  35273  trlset  35274  trlval  35275  tgrpfset  35858  tgrpset  35859  tendofset  35872  tendoset  35873  tendo02  35901  tendoi  35908  erngfset  35913  erngset  35914  erngfset-rN  35921  erngset-rN  35922  cdlemksv  35958  dvafset  36118  dvaset  36119  dvaplusgv  36124  diaffval  36145  diafval  36146  diaval  36147  dvhfset  36195  dvhset  36196  cdlemm10N  36233  docaffvalN  36236  docafvalN  36237  djaffvalN  36248  djafvalN  36249  dibffval  36255  dibfval  36256  dibval  36257  dicffval  36289  dicfval  36290  dicval  36291  dihffval  36345  dihfval  36346  dihval  36347  dochffval  36464  dochfval  36465  djhffval  36511  djhfval  36512  dochfl1  36591  lpolsetN  36597  lcfrlem8  36664  lcdfval  36703  lcdval  36704  mapdffval  36741  mapdfval  36742  mapdhval  36839  hvmapffval  36873  hvmapfval  36874  hdmap1ffval  36911  hdmap1fval  36912  hdmapffval  36944  hdmapfval  36945  hgmapffval  37003  hgmapfval  37004  isnacs  37093  mzpclval  37114  mzpsubst  37137  mzprename  37138  mzpcompact2lem  37140  eldiophb  37146  diophrw  37148  eldioph2  37151  diophin  37162  diophun  37163  diophren  37203  pell1qrval  37236  pell14qrval  37238  pell1234qrval  37240  pellfundval  37270  rmxypairf1o  37302  rmxyval  37306  mzpcong  37365  pw2f1ocnv  37430  dnnumch1  37440  dfac11  37458  hbtlem1  37519  hbtlem7  37521  elmnc  37532  dgraaval  37540  mpaaval  37547  itgoval  37557  rgspnval  37564  flcidc  37570  mendval  37579  issdrg  37593  mon1pid  37609  cytpval  37613  elcnvlem  37733  comptiunov2i  37824  dftrcl3  37838  trclfvcom  37841  cnvtrclfv  37842  cotrcltrcl  37843  trclimalb2  37844  trclfvdecomr  37846  dfrtrcl3  37851  dfrtrcl4  37856  clsk1indlem0  38165  clsk1indlem2  38166  clsk1indlem3  38167  clsk1indlem4  38168  clsk1indlem1  38169  k0004val  38274  lhe4.4ex1a  38354  addrfv  38499  subrfv  38500  mulvfv  38501  sumnnodd  39668  liminfgval  39794  ioodvbdlimc2lem  39918  itgsin0pilem1  39934  stoweidlem55  40041  wallispilem1  40051  wallispilem2  40052  wallispilem4  40054  wallispi2lem1  40057  wallispi2lem2  40058  dirkerval  40077  fourierdlem2  40095  fourierdlem3  40096  fourierdlem29  40122  fourierdlem62  40154  fourierdlem80  40172  fourierdlem103  40195  fourierdlem104  40196  fourierswlem  40216  fouriersw  40217  iundjiunlem  40445  carageniuncllem2  40505  0ome  40512  hoidmv1le  40577  hoidmvlelem3  40580  smflimsuplem7  40801  issubmgm  41560  vsetrec  42217  onsetreclem1  42219  elpglem3  42227  sinhval-named  42248  coshval-named  42249  tanhval-named  42250  secval  42259  cscval  42260  cotval  42261  aacllem  42318
  Copyright terms: Public domain W3C validator