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

Theorem fvmpt 7015
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 7013 . 2 ((𝐴𝐷𝐶 ∈ V) → (𝐹𝐴) = 𝐶)
51, 4mpan2 691 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  wcel 2105  Vcvv 3477  cmpt 5230  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570
This theorem is referenced by:  fvmptex  7029  fvmptrabfv  7047  mptfvmpt  7247  fvmptopab  7486  ofval  7707  caofinvl  7728  fvresex  7982  1stval  8014  2ndval  8015  reldm  8067  curry1val  8128  curry2val  8132  fsplitfpar  8141  fnwelem  8154  brtpos2  8255  onovuni  8380  tz7.44-1  8444  oasuc  8560  oesuclem  8561  omsuc  8562  onasuc  8564  onmsuc  8565  fsetfocdm  8899  fvmptmap  8919  xpcomco  9100  unxpdomlem1  9283  unfilem2  9341  ordtypelem3  9557  ixpiunwdom  9627  inf3lema  9661  noinfep  9697  cantnfval  9705  cantnflem1d  9725  cantnflem1  9726  ssttrcl  9752  ttrcltr  9753  ttrclselem2  9763  r1sucg  9806  r0weon  10049  infxpenc2lem1  10056  fseqenlem1  10061  fseqenlem2  10062  dfac8alem  10066  ac5num  10073  acni2  10083  dfac4  10159  dfac2a  10167  dfacacn  10179  dfac12lem1  10181  ackbij1lem7  10262  ackbij2lem2  10276  ackbij2lem3  10277  cfsmolem  10307  fin23lem28  10377  fin23lem39  10387  isf32lem6  10395  isf32lem7  10396  isf32lem8  10397  fin1a2lem3  10439  itunifval  10453  itunisuc  10456  axdc2lem  10485  axdc3lem2  10488  axcclem  10494  zorn2lem1  10533  negiso  12245  infrenegsup  12248  uzval  12877  flval  13830  ceilval  13874  ceilval2  13876  monoord2  14070  seqf1olem2  14079  seqf1o  14080  seqdistr  14090  serle  14094  seqof  14096  swrdfv  14682  revval  14794  revfv  14797  wwlktovf1  14992  wwlktovfo  14993  sgnval  15123  cjval  15137  reval  15141  imval  15142  sqrtval  15272  absval  15273  limsupval  15506  limsupgval  15508  climmpt  15603  climle  15672  rlimdiv  15678  isercolllem1  15697  isercoll2  15701  caurcvg2  15710  fsumser  15762  isumadd  15799  fsumcnv  15805  fsumrev  15811  fsumshft  15812  iserabs  15847  cvgcmp  15848  cvgcmpce  15850  incexclem  15868  isumless  15877  divcnvshft  15887  supcvg  15888  harmonic  15891  trireciplem  15894  trirecip  15895  expcnv  15896  explecnv  15897  geolim  15902  geolim2  15903  geo2lim  15907  geomulcvg  15908  geoisum  15909  geoisumr  15910  geoisum1  15911  geoisum1c  15912  cvgrat  15915  mertenslem2  15917  mertens  15918  prodfdiv  15928  fprodser  15981  fprodshft  16008  fprodrev  16009  fprodcnv  16015  iprodmul  16035  bpolylem  16080  eftval  16108  efval  16111  efcvgfsum  16118  ege2le3  16122  eftlub  16141  eflegeo  16153  sinval  16154  cosval  16155  tanval  16160  eirrlem  16236  rpnnen2lem1  16246  rpnnen2lem2  16247  bitsfval  16456  bitsinv2  16476  bitsinv  16481  sadcf  16486  sadc0  16487  sadcp1  16488  smupf  16511  smup0  16512  smupp1  16513  qnumval  16770  qdenval  16771  phival  16800  crth  16811  phimullem  16812  eulerthlem2  16815  phisum  16823  odzval  16824  iserodd  16868  pcmpt  16925  prmreclem1  16949  prmreclem2  16950  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  1arithlem1  16956  1arithlem2  16957  vdwapfval  17004  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  ramub1lem2  17060  ramcl  17062  prmoval  17066  strfvnd  17218  topnval  17480  prdsplusgfval  17520  prdsmulrfval  17522  isacs  17695  acsfn  17703  homffval  17734  comfffval  17742  oppcval  17757  monfval  17779  oppcmon  17785  sectffval  17797  invffval  17805  isoval  17812  idfuval  17926  homafval  18082  arwval  18096  coafval  18117  yonedainv  18337  oduval  18344  pltfval  18388  lubfval  18407  lubval  18413  glbfval  18420  glbval  18426  p0val  18484  p1val  18485  ipoval  18587  plusffval  18671  grpidval  18686  issubmgm  18727  issubm  18828  prdspjmhm  18854  efmnd  18895  smndex1igid  18929  grpinvfval  19008  grpinvval  19010  grpsubfval  19013  grpsubfvalALT  19014  grplactval  19072  prdsinvlem  19079  mulgfval  19099  mulgfvalALT  19100  pwsmulg  19149  issubg  19156  isnsg  19185  cycsubmel  19230  cycsubgcl  19236  conjghm  19279  conjnmz  19282  cntrval  19349  cntzfval  19350  cntzval  19351  oppgval  19377  psgnfval  19532  psgnval  19539  odfval  19564  odval  19566  sylow1lem4  19633  pgpssslw  19646  sylow2blem3  19654  sylow3lem2  19660  lsmfval  19670  pj1fval  19726  efgval  19749  efgsval  19763  frgpval  19790  vrgpval  19799  mulgmhm  19859  mulgghm  19860  ablfaclem1  20119  mgpval  20154  srglmhm  20238  srgrmhm  20239  ringlghm  20325  ringrghm  20326  pwspjmhmmgpd  20341  pwsexpg  20342  opprval  20351  dvdsrval  20377  isunit  20389  invrfval  20405  dvrfval  20418  isirred  20435  issubrng  20563  issubrg  20587  rgspnval  20628  rrgval  20713  fidomndrnglem  20789  issdrg  20805  abvfval  20827  abvtrivd  20849  staffval  20858  stafval  20859  scaffval  20894  lmodvsghm  20937  lssset  20948  lspfval  20988  islbs  21092  sraval  21191  rlmval  21215  2idlval  21278  lpival  21351  expmhm  21471  expghm  21503  mulgghm2  21504  mulgrhm  21505  zrhval  21535  zrhmulg  21537  zlmval  21543  chrval  21555  znval  21567  znzrhval  21582  evpmss  21621  psgnevpmb  21622  ip0l  21671  ipffval  21683  ocvfval  21701  ocvval  21702  cssval  21717  thlval  21730  pjfval  21743  pjval  21747  isobs  21757  prdsinvgd2  21779  uvcresum  21830  frlmup1  21835  frlmup2  21836  islinds  21846  islindf5  21876  aspval  21910  asclval  21917  psrmulval  21981  psrlidm  21999  psrridm  22000  psrascl  22016  mvrval  22019  mvrval2  22020  mplmonmul  22071  evlslem3  22121  evlslem1  22123  evlsval  22127  evlssca  22130  evlsvar  22131  psdmul  22187  psr1val  22202  vr1val  22208  ply1val  22210  coe1fval  22222  coe1fv  22223  coe1tmmul2  22294  coe1tmmul  22295  coe1tmmul2fv  22296  coe1pwmulfv  22298  evls1val  22339  evl1fval  22347  evl1val  22348  mamulid  22462  mamurid  22463  mdetleib  22608  mdetleib1  22612  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  cpmidpmatlem1  22891  ordtval  23212  cnpval  23259  ptpjpre1  23594  ptpjopn  23635  dfac14  23641  upxp  23646  uptx  23648  hauseqlcld  23669  txlm  23671  xkoptsub  23677  xkoinjcn  23710  kqval  23749  xpstopnlem1  23832  fmval  23966  flfval  24013  ptcmplem2  24076  ptcmplem3  24077  symgtgp  24129  qustgpopn  24143  ussval  24283  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  mopnval  24463  prdsxmslem2  24557  nmfval  24616  nmval  24617  nmoval  24751  metdsval  24882  divcnOLD  24903  divcn  24905  mulc1cncf  24944  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  cnheiborlem  24999  evth  25004  evth2  25005  lebnumlem3  25008  isphtpy  25026  isphtpc  25039  pcofval  25056  pcovalg  25058  pco1  25061  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevcl  25071  pcorevlem  25072  pcorev2  25074  pi1xfrcnv  25103  cphnm  25240  tcphval  25265  tcphnmval  25276  cfilfval  25311  iscmet  25331  iscmet3lem3  25337  rrxval  25434  ehlval  25461  ivth2  25503  ovolval  25521  ovollb2lem  25536  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliunlem2  25551  ovolicc1  25564  voliunlem1  25598  voliunlem2  25599  voliunlem3  25600  volsup  25604  ioorval  25622  uniioombllem3  25633  uniioombllem6  25636  volsup2  25653  volcn  25654  volivth  25655  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  vitali  25661  mbfmax  25697  mbfimaopnlem  25703  itg1val  25731  i1f1lem  25737  itg11  25739  itg1addlem4  25747  itg1addlem4OLD  25748  itg1mulc  25753  i1fres  25754  itg1climres  25763  mbfi1fseqlem2  25765  mbfi1fseqlem3  25766  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfi1flim  25772  mbfmullem2  25773  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  itg2cnlem1  25810  itg2cn  25812  limccnp2  25941  dvnff  25973  dvnp1  25975  cpnfval  25982  elcpn  25984  dvrec  26007  dvcnvlem  26028  dveflem  26031  dvef  26032  dvferm1  26037  dvferm2  26039  rolle  26042  dvlip  26046  dvlipcn  26047  dv11cn  26054  dvivthlem1  26061  dvivth  26063  lhop1lem  26066  ftc1lem1  26090  ftc1lem5  26095  ftc2  26099  itgsubstlem  26103  tdeglem3  26112  tdeglem4  26113  mdegval  26116  mdegmullem  26131  deg1fval  26133  deg1ldg  26145  deg1leb  26148  coe1mul3  26152  uc1pval  26193  mon1pval  26195  mon1pid  26207  q1pval  26208  r1pval  26211  ply1remlem  26218  ig1pval  26229  plyval  26246  elply2  26249  plyeq0lem  26263  coeval  26276  dgrval  26281  coeid2  26292  coemullem  26303  coemul  26305  elqaalem1  26375  elqaalem2  26376  elqaalem3  26377  iaa  26381  aareccl  26382  aannenlem1  26384  geolim3  26395  aaliou3lem1  26398  aaliou3lem2  26399  aaliou3lem5  26403  aaliou3lem6  26404  aaliou3lem7  26405  aaliou3  26407  tayl0  26417  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmshftlem  26446  ulmshft  26447  ulmuni  26449  ulmcau  26452  ulmdvlem1  26457  ulmdvlem3  26459  mtest  26461  mtestbdd  26462  mbfulm  26463  iblulm  26464  itgulm  26465  pserval  26467  pserval2  26468  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  pserulm  26479  pserdvlem2  26486  pserdv  26487  abelthlem1  26489  abelthlem3  26491  abelthlem4  26492  abelthlem5  26493  abelthlem6  26494  abelthlem7  26496  abelthlem8  26497  abelthlem9  26498  resinf1o  26592  efif1olem4  26601  eff1olem  26604  logcnlem5  26702  logtayllem  26715  logtayl  26716  logtaylsum  26717  logtayl2  26718  logccv  26719  asinval  26939  acosval  26940  atanval  26941  atantayl  26994  leibpilem2  26998  leibpi  26999  leibpisum  27000  log2cnv  27001  log2tlbnd  27002  areaval  27021  efrlim  27026  efrlimOLD  27027  dfef2  27028  amgmlem  27047  emcllem2  27054  emcllem3  27055  emcllem4  27056  emcllem5  27057  emcllem6  27058  emcllem7  27059  zetacvg  27072  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulm2  27093  lgamcvglem  27097  igamval  27104  lgamcvg2  27112  gamcvg2lem  27116  ftalem7  27136  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  basellem6  27143  basellem8  27145  basellem9  27146  chtval  27167  vmaval  27170  chpval  27179  ppival  27184  muval  27189  prmorcht  27235  sqff1o  27239  dvdsflsumcom  27245  musum  27248  muinv  27250  sgmppw  27255  fsumvma  27271  pclogsum  27273  dchrfi  27313  bposlem5  27346  bposlem7  27348  bposlem8  27349  bposlem9  27350  lgsfval  27360  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  lgsqrlem2  27405  lgsqrlem4  27407  lgseisenlem2  27434  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasumiflem1  27559  dchrvmaeq0  27562  dchrisum0fval  27563  dchrisum0re  27571  mulog2sumlem1  27592  pntrval  27620  pntsval  27630  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntlem3  27667  abvcxp  27673  padicfval  27674  padicval  27675  padicabv  27688  ostth1  27691  ostth2  27695  ostth3  27696  nosupfv  27765  noinffv  27780  newval  27908  leftval  27916  rightval  27917  iscgrg  28534  legval  28606  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  iseqlg  28889  ttgval  28897  ttgvalOLD  28898  elee  28923  axsegconlem1  28946  axsegconlem9  28954  axsegconlem10  28955  axpasch  28970  axlowdimlem15  28985  axlowdim  28990  axeuclidlem  28991  axcontlem2  28994  eengv  29008  vtxval  29031  iedgval  29032  edgval  29080  vtxdgval  29500  wwlksnextinj  29928  wwlksnextsurj  29929  clwwlkfv  30076  clwwlknonmpo  30117  fusgreg2wsplem  30361  fusgreghash2wsp  30366  numclwwlk1lem2fv  30384  gidval  30540  grpoinvval  30551  bafval  30632  imsval  30713  dipfval  30730  sspval  30751  nmooval  30791  hmoval  30838  ipasslem8  30865  ipasslem9  30866  ipblnfi  30883  ubthlem2  30899  htthlem  30945  normval  31152  ocval  31308  occllem  31331  hsupval  31362  pjhfval  31424  pjhval  31425  chscllem2  31666  chscllem3  31667  hosval  31768  homval  31769  hodval  31770  hfsval  31771  hfmval  31772  brafval  31971  braval  31972  kbval  31982  eigvalval  31988  cnlnadjlem1  32095  nmopadjlei  32116  hmopidmchi  32179  strlem2  32279  hstrlem2  32287  cdj3lem2  32463  ofpreima  32681  psgnfzto1stlem  33102  evpmval  33147  altgnsg  33151  inftmrel  33169  isinftm  33170  qusker  33356  qusvscpbl  33358  qusvsval  33359  mxidlval  33468  idlsrgval  33510  dimval  33627  dimvalfi  33628  smatfval  33755  lmatval  33773  locfinreflem  33800  rspecval  33824  rmulccn  33888  xrmulc1cn  33890  xrge0iifcv  33894  xrge0iifiso  33895  xrge0iifhom  33897  xrge0iif1  33898  qqhval  33934  rrhval  33958  xrhval  33980  ddeval1  34214  ddeval0  34215  sxbrsigalem0  34252  sxbrsigalem3  34253  eulerpartlemgv  34354  rrvmbfm  34423  dstrvval  34451  coinflippv  34464  ballotlem2  34469  ballotlemfval  34470  ballotlemi  34481  ballotlemsval  34489  ballotlemrval  34498  ballotth  34518  plymulx  34541  signstfv  34556  signsvvfval  34571  derangval  35151  subfacval  35157  erdszelem3  35177  erdszelem9  35183  erdszelem10  35184  txpconn  35216  indispconn  35218  cvxpconn  35226  cvmlift2lem2  35288  cvmlift2lem3  35289  cvmlift2lem7  35293  cvmliftphtlem  35301  cvmlift3lem4  35306  snmlfval  35314  snmlval  35315  gonafv  35334  mvtval  35484  mrsubffval  35491  mrsubcv  35494  mrsubrn  35497  elmrsubrn  35504  msubffval  35507  mvhval  35518  mpstval  35519  mstaval  35528  mclsval  35547  mppsval  35556  sinccvglem  35656  circum  35658  divcnvlin  35712  iprodefisum  35720  iprodgam  35721  faclimlem1  35722  faclimlem2  35723  faclim  35725  iprodfac  35726  faclim2  35727  dfrdg2  35776  findabrcl  36436  dnival  36453  bj-evalval  37057  bj-inftyexpitaudisj  37187  bj-inftyexpiinv  37190  bj-inftyexpidisj  37192  curfv  37586  finixpnum  37591  poimirlem16  37622  poimir  37639  broucube  37640  mblfinlem2  37644  voliunnfl  37650  volsupnfl  37651  itg2addnclem  37657  itg2addnclem3  37659  ftc1cnnc  37678  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  ftc2nc  37688  fvopabf4g  37708  sdclem2  37728  fdc  37731  lmclim2  37744  geomcau  37745  istotbnd  37755  isbnd  37766  prdsbnd2  37781  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  rrnval  37813  rrncmslem  37818  idlval  37999  pridlval  38019  maxidlval  38025  lshpset  38959  lsatset  38971  lcvfbr  39001  lflset  39040  lflnegcl  39056  lshpkrlem1  39091  lshpkrlem2  39092  lshpkrlem3  39093  ldualset  39106  cmtfvalN  39191  cvrfval  39249  pats  39266  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  pointsetN  39723  psubspset  39726  pmapval  39739  paddfval  39779  pclfvalN  39871  polfvalN  39886  polvalN  39887  psubclsetN  39918  watvalN  39975  lhpset  39977  lautset  40064  pautsetN  40080  ldilset  40091  ltrnset  40100  dilsetN  40135  trnsetN  40138  trlset  40143  trlval  40144  tgrpset  40727  tendoset  40741  tendo02  40769  erngset  40782  erngset-rN  40790  cdlemksv  40826  dvaset  40987  dvaplusgv  40992  diafval  41013  diaval  41014  dvhset  41063  cdlemm10N  41100  docafvalN  41104  djafvalN  41116  dibfval  41123  dibval  41124  dicfval  41157  dicval  41158  dihval  41214  dochfval  41332  djhfval  41379  dochfl1  41458  lpolsetN  41464  lcdval  41571  mapdhval  41706  hvmapfval  41741  hdmap1fval  41778  fimgmcyc  42520  prjspval  42589  isnacs  42691  mzpclval  42712  mzpsubst  42735  mzprename  42736  mzpcompact2lem  42738  eldiophb  42744  diophrw  42746  eldioph2  42749  diophin  42759  diophun  42760  diophren  42800  pell1qrval  42833  pell14qrval  42835  pell1234qrval  42837  pellfundval  42867  rmxypairf1o  42899  rmxyval  42903  mzpcong  42960  pw2f1ocnv  43025  dnnumch1  43032  dfac11  43050  hbtlem1  43111  hbtlem7  43113  elmnc  43124  dgraaval  43132  mpaaval  43139  itgoval  43149  flcidc  43158  mendval  43167  cytpval  43190  cantnfub  43310  cantnfresb  43313  tfsconcatrev  43337  elcnvlem  43590  comptiunov2i  43695  dftrcl3  43709  trclfvcom  43712  cnvtrclfv  43713  cotrcltrcl  43714  trclimalb2  43715  trclfvdecomr  43717  dfrtrcl3  43722  dfrtrcl4  43727  clsk1indlem0  44030  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  k0004val  44139  lhe4.4ex1a  44324  addrfv  44464  subrfv  44465  mulvfv  44466  monoord2xrv  45433  sumnnodd  45585  liminfgval  45717  ioodvbdlimc2lem  45889  itgsin0pilem1  45905  stoweidlem55  46010  wallispilem1  46020  wallispilem2  46021  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  dirkerval  46046  fourierdlem2  46064  fourierdlem3  46065  fourierdlem29  46091  fourierdlem62  46123  fourierdlem80  46141  fourierdlem103  46164  fourierdlem104  46165  fourierswlem  46185  fouriersw  46186  iundjiunlem  46414  carageniuncllem2  46477  0ome  46484  hoidmv1le  46549  hoidmvlelem3  46552  smflimsuplem7  46781  iccpval  47339  fppr  47650  bigoval  48398  ackval0  48529  ackval41a  48543  eenglngeehlnm  48588  prstcval  48864  mndtcval  48887  vsetrec  48933  onsetreclem1  48935  elpglem3  48943  pgindnf  48946  sinhval-named  48966  coshval-named  48967  tanhval-named  48968  secval  48977  cscval  48978  cotval  48979  aacllem  49031
  Copyright terms: Public domain W3C validator