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

Theorem fvmpt 5797
Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
Hypotheses
Ref Expression
fvmptg.1  |-  ( x  =  A  ->  B  =  C )
fvmptg.2  |-  F  =  ( x  e.  D  |->  B )
fvmpt.3  |-  C  e. 
_V
Assertion
Ref Expression
fvmpt  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Distinct variable groups:    x, A    x, C    x, D
Allowed substitution hints:    B( x)    F( x)

Proof of Theorem fvmpt
StepHypRef Expression
1 fvmpt.3 . 2  |-  C  e. 
_V
2 fvmptg.1 . . 3  |-  ( x  =  A  ->  B  =  C )
3 fvmptg.2 . . 3  |-  F  =  ( x  e.  D  |->  B )
42, 3fvmptg 5795 . 2  |-  ( ( A  e.  D  /\  C  e.  _V )  ->  ( F `  A
)  =  C )
51, 4mpan2 653 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   _Vcvv 2948    e. cmpt 4258   ` cfv 5445
This theorem is referenced by:  fvmptex  5806  fvresex  5973  ofval  6305  caofinvl  6322  1stval  6342  2ndval  6343  reldm  6389  curry1val  6430  curry2val  6434  fnwelem  6452  brtpos2  6476  onovuni  6595  tz7.44-1  6655  oasuc  6759  oesuclem  6760  omsuc  6761  onasuc  6763  onmsuc  6764  fvmptmap  7041  xpcomco  7189  unxpdomlem1  7304  unfilem2  7363  ordtypelem3  7478  ixpiunwdom  7548  inf3lema  7568  noinfep  7603  cantnfval  7612  cantnflem1d  7633  cantnflem1  7634  r1sucg  7684  r0weon  7883  infxpenc2lem1  7889  fseqenlem1  7894  fseqenlem2  7895  dfac8alem  7899  ac5num  7906  acni2  7916  dfac4  7992  dfac2a  7999  dfacacn  8010  dfac12lem1  8012  ackbij1lem7  8095  ackbij2lem2  8109  ackbij2lem3  8110  cfsmolem  8139  fin23lem28  8209  fin23lem39  8219  isf32lem6  8227  isf32lem7  8228  isf32lem8  8229  fin1a2lem3  8271  itunifval  8285  itunisuc  8288  axdc2lem  8317  axdc3lem2  8320  axcclem  8326  zorn2lem1  8365  negiso  9973  infmsup  9975  uzval  10479  flval  11191  monoord2  11342  seqf1olem2  11351  seqf1o  11352  seqdistr  11362  serle  11366  seqof  11368  swrdfv  11759  revval  11780  revfv  11783  cjval  11895  reval  11899  imval  11900  sqrval  12030  absval  12031  limsupval  12256  limsupgval  12258  climmpt  12353  climle  12421  rlimdiv  12427  isercolllem1  12446  isercoll2  12450  caurcvg2  12459  fsumser  12512  isumadd  12539  fsumcnv  12545  fsumrev  12550  fsumshft  12551  iserabs  12582  cvgcmp  12583  cvgcmpce  12585  incexclem  12604  isumless  12613  supcvg  12623  harmonic  12626  trireciplem  12629  trirecip  12630  expcnv  12631  explecnv  12632  geolim  12635  geolim2  12636  geo2lim  12640  geomulcvg  12641  geoisum  12642  geoisumr  12643  geoisum1  12644  geoisum1c  12645  cvgrat  12648  mertenslem2  12650  mertens  12651  eftval  12667  efval  12670  efcvgfsum  12676  ege2le3  12680  eftlub  12698  eflegeo  12710  sinval  12711  cosval  12712  tanval  12717  eirrlem  12791  rpnnen2lem1  12802  rpnnen2lem2  12803  bitsfval  12923  bitsinv2  12943  bitsinv  12948  sadcf  12953  sadc0  12954  sadcp1  12955  smupf  12978  smup0  12979  smupp1  12980  qnumval  13117  qdenval  13118  phival  13144  crt  13155  phimullem  13156  eulerthlem2  13159  odzval  13165  iserodd  13197  pcmpt  13249  prmreclem1  13272  prmreclem2  13273  prmreclem4  13275  prmreclem5  13276  prmreclem6  13277  1arithlem1  13279  1arithlem2  13280  vdwapfval  13327  vdwlem2  13338  vdwlem6  13342  vdwlem8  13344  vdwlem9  13345  ramub1lem2  13383  ramcl  13385  strfvnd  13472  topnval  13650  prdsplusgfval  13684  prdsmulrfval  13686  isacs  13864  acsfn  13872  cidfval  13889  homffval  13905  comfffval  13912  oppcval  13927  monfval  13946  oppcmon  13952  sectffval  13964  invffval  13971  isoval  13978  idfuval  14061  homafval  14172  arwval  14186  idafval  14200  coafval  14207  yonedainv  14366  pltfval  14404  lubfval  14423  lubval  14424  glbfval  14428  glbval  14429  joinfval  14432  meetfval  14439  p0val  14458  p1val  14459  oduval  14545  ipoval  14568  plusffval  14690  grpidval  14695  issubm  14736  prdspjmhm  14754  grpinvfval  14831  grpinvval  14832  grpsubfval  14835  grplactfval  14873  grplactval  14874  mulgfval  14879  prdsinvlem  14914  pwsmulg  14920  issubg  14932  cycsubgcl  14954  isnsg  14957  conjghm  15024  conjnmz  15027  symgval  15082  cntrval  15106  cntzfval  15107  cntzval  15108  oppgval  15131  odfval  15159  odval  15160  sylow1lem4  15223  pgpssslw  15236  sylow2blem3  15244  sylow3lem2  15250  lsmfval  15260  pj1fval  15314  efgval  15337  efgsval  15351  frgpval  15378  vrgpval  15387  mulgmhm  15438  mulgghm  15439  ablfaclem1  15631  mgpval  15639  rnglghm  15699  rngrghm  15700  opprval  15717  dvdsrval  15738  isunit  15750  invrfval  15766  dvrfval  15777  isirred  15792  issubrg  15856  abvfval  15894  abvtrivd  15916  staffval  15923  stafval  15924  scaffval  15956  lmodvsghm  15993  lssset  15998  lspfval  16037  islbs  16136  sraval  16236  rlmval  16252  2idlval  16292  lpival  16304  rrgval  16335  fidomndrnglem  16354  aspval  16375  asclfval  16381  asclval  16382  psrmulval  16438  psrlidm  16455  psrridm  16456  mvrval  16473  mvrval2  16474  mplmonmul  16515  psr1val  16572  vr1val  16578  ply1val  16580  coe1fval  16591  coe1fv  16592  coe1tmmul2  16656  coe1tmmul  16657  coe1tmmul2fv  16658  coe1pwmulfv  16660  expmhm  16764  expghm  16765  mulgghm2  16774  mulgrhm  16775  zrhval  16777  zrhmulg  16779  zlmval  16785  chrval  16794  znval  16804  znzrhval  16815  ip0l  16855  ipffval  16867  ocvfval  16881  ocvval  16882  cssval  16897  thlval  16910  pjfval  16921  pjval  16925  isobs  16935  ordtval  17241  cnpval  17288  ptpjpre1  17591  ptpjopn  17632  dfac14  17638  upxp  17643  uptx  17645  hauseqlcld  17666  txlm  17668  xkoptsub  17674  xkoinjcn  17707  kqval  17746  xpstopnlem1  17829  fmval  17963  flfval  18010  ptcmplem2  18072  ptcmplem3  18073  symgtgp  18119  divstgpopn  18137  ussval  18277  iscfilu  18306  ispsmet  18323  ismet  18341  isxmet  18342  mopnval  18456  prdsxmslem2  18547  nmfval  18624  nmval  18625  nmoval  18737  metdsval  18865  divcn  18886  mulc1cncf  18923  icopnfhmeo  18956  iccpnfhmeo  18958  xrhmeo  18959  cnheiborlem  18967  evth  18972  evth2  18973  lebnumlem3  18976  isphtpy  18994  isphtpc  19007  pcofval  19023  pcovalg  19025  pco1  19028  pcopt  19035  pcopt2  19036  pcoass  19037  pcorevcl  19038  pcorevlem  19039  pcorev2  19041  pi1xfrcnv  19070  cphnm  19144  tchval  19165  tchnmval  19175  cfilfval  19205  iscmet  19225  iscmet3lem3  19231  ivth2  19340  ovolval  19358  ovollb2lem  19372  ovolunlem1a  19380  ovolunlem1  19381  ovoliunlem1  19386  ovoliunlem2  19387  ovolicc1  19400  voliunlem1  19432  voliunlem2  19433  voliunlem3  19434  volsup  19438  ioorval  19454  uniioombllem3  19465  uniioombllem6  19468  volsup2  19485  volcn  19486  volivth  19487  vitalilem2  19489  vitalilem3  19490  vitalilem4  19491  vitali  19493  mbfmax  19529  mbfimaopnlem  19535  itg1val  19563  i1f1lem  19569  itg11  19571  itg1addlem4  19579  itg1mulc  19584  i1fres  19585  itg1climres  19594  mbfi1fseqlem2  19596  mbfi1fseqlem3  19597  mbfi1fseqlem6  19600  mbfi1flimlem  19602  mbfi1flim  19603  mbfmullem2  19604  itg2seq  19622  itg2uba  19623  itg2splitlem  19628  itg2monolem1  19630  itg2monolem2  19631  itg2monolem3  19632  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq  19635  itg2i1fseq2  19636  itg2addlem  19638  itg2cnlem1  19641  itg2cn  19643  limccnp2  19767  dvnff  19797  dvnp1  19799  cpnfval  19806  elcpn  19808  dvrec  19829  dvcnvlem  19848  dveflem  19851  dvef  19852  dvferm1  19857  dvferm2  19859  rolle  19862  dvlip  19865  dvlipcn  19866  dv11cn  19873  dvivthlem1  19880  dvivth  19882  lhop1lem  19885  ftc1lem1  19907  ftc1lem5  19912  ftc2  19916  itgsubstlem  19920  evlslem3  19923  evlslem1  19924  evlsval  19928  evlssca  19931  evlsvar  19932  evl1fval  19935  evl1val  19936  tdeglem3  19970  tdeglem4  19971  mdegval  19974  mdegmullem  19989  deg1fval  19991  deg1ldg  20003  deg1leb  20006  coe1mul3  20010  uc1pval  20050  mon1pval  20052  q1pval  20064  r1pval  20067  ply1remlem  20073  ig1pval  20083  plyval  20100  elply2  20103  plyeq0lem  20117  coeval  20130  dgrval  20135  coeid2  20146  coemullem  20156  coemul  20158  elqaalem1  20224  elqaalem2  20225  elqaalem3  20226  iaa  20230  aareccl  20231  aannenlem1  20233  geolim3  20244  aaliou3lem1  20247  aaliou3lem2  20248  aaliou3lem5  20252  aaliou3lem6  20253  aaliou3lem7  20254  aaliou3  20256  tayl0  20266  taylthlem1  20277  taylthlem2  20278  ulmshftlem  20293  ulmshft  20294  ulmuni  20296  ulmcau  20299  ulmdvlem1  20304  ulmdvlem3  20306  mtest  20308  mtestbdd  20309  mbfulm  20310  iblulm  20311  itgulm  20312  pserval  20314  pserval2  20315  radcnvlem1  20317  radcnvlem2  20318  dvradcnv  20325  pserulm  20326  pserdvlem2  20332  pserdv  20333  abelthlem1  20335  abelthlem3  20337  abelthlem4  20338  abelthlem5  20339  abelthlem6  20340  abelthlem7  20342  abelthlem8  20343  abelthlem9  20344  resinf1o  20426  efgh  20431  efif1olem4  20435  eff1olem  20438  logcnlem5  20525  logtayllem  20538  logtayl  20539  logtaylsum  20540  logtayl2  20541  logccv  20542  asinval  20710  acosval  20711  atanval  20712  atantayl  20765  leibpilem2  20769  leibpi  20770  leibpisum  20771  log2cnv  20772  log2tlbnd  20773  areaval  20791  efrlim  20796  dfef2  20797  amgmlem  20816  emcllem2  20823  emcllem3  20824  emcllem4  20825  emcllem5  20826  emcllem6  20827  emcllem7  20828  ftalem7  20849  basellem2  20852  basellem3  20853  basellem4  20854  basellem5  20855  basellem6  20856  basellem8  20858  basellem9  20859  chtval  20881  vmaval  20884  chpval  20893  ppival  20898  muval  20903  prmorcht  20949  sqff1o  20953  dvdsflsumcom  20961  musum  20964  muinv  20966  sgmppw  20969  fsumvma  20985  pclogsum  20987  dchrfi  21027  bposlem5  21060  bposlem7  21062  bposlem8  21063  bposlem9  21064  lgsfval  21073  lgsdir  21102  lgsdilem2  21103  lgsdi  21104  lgsne0  21105  lgsqrlem2  21114  lgsqrlem4  21116  lgseisenlem2  21122  dchrmusum2  21176  dchrvmasumlem1  21177  dchrvmasumiflem1  21183  dchrvmaeq0  21186  dchrisum0fval  21187  dchrisum0re  21195  mulog2sumlem1  21216  pntrval  21244  pntsval  21254  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntlem3  21291  abvcxp  21297  padicfval  21298  padicval  21299  padicabv  21312  ostth1  21315  ostth2  21319  ostth3  21320  vdgrval  21655  gidval  21789  grpoinvval  21801  bafval  22071  imsval  22165  dipfval  22186  sspval  22210  nmooval  22252  hmoval  22299  ipasslem8  22326  ipasslem9  22327  ipblnfi  22345  ubthlem2  22361  htthlem  22408  normval  22614  ocval  22770  occllem  22793  hsupval  22824  pjhfval  22886  pjhval  22887  chscllem2  23128  chscllem3  23129  hosval  23231  homval  23232  hodval  23233  hfsval  23234  hfmval  23235  brafval  23434  braval  23435  kbval  23445  eigvalval  23451  cnlnadjlem1  23558  nmopadjlei  23579  hmopidmchi  23642  strlem2  23742  hstrlem2  23750  cdj3lem2  23926  ofpreima  24069  inftmrel  24238  isinftm  24239  rmulccn  24302  xrmulc1cn  24304  xrge0iifcv  24308  xrge0iifiso  24309  xrge0iifhom  24311  xrge0iif1  24312  qqhval  24346  rrhval  24367  xrhval  24372  sxbrsigalem0  24609  sxbrsigalem3  24610  rrvmbfm  24688  dstrvval  24716  coinflippv  24729  ballotlem2  24734  ballotlemfval  24735  ballotlemi  24746  ballotlemsval  24754  ballotlemrval  24763  ballotth  24783  zetacvg  24787  lgamgulmlem4  24804  lgamgulmlem5  24805  lgamgulm2  24808  lgamcvglem  24812  igamval  24819  lgamcvg2  24827  gamcvg2lem  24831  derangval  24841  subfacval  24847  erdszelem3  24867  erdszelem9  24873  erdszelem10  24874  txpcon  24907  indispcon  24909  cvxpcon  24917  cvmlift2lem2  24979  cvmlift2lem3  24980  cvmlift2lem7  24984  cvmliftphtlem  24992  cvmlift3lem4  24997  snmlfval  25005  snmlval  25006  sinccvglem  25097  circum  25099  divcnvshft  25199  divcnvlin  25200  prodfdiv  25213  fprodser  25264  fprodshft  25289  fprodrev  25290  fprodcnv  25296  iprodmul  25305  iprodefisum  25307  iprodgam  25308  faclimlem1  25351  faclimlem2  25352  faclim  25354  iprodfac  25355  faclim2  25356  dfrdg2  25407  elee  25781  axsegconlem1  25804  axsegconlem9  25812  axsegconlem10  25813  axpasch  25828  axlowdimlem15  25843  axlowdim  25848  axeuclidlem  25849  axcontlem2  25852  bpolylem  26042  findabrcl  26152  mblfinlem  26190  voliunnfl  26196  volsupnfl  26197  itg2addnclem  26202  itg2addnclem3  26204  ftc1cnnc  26225  fvopabf4g  26359  sdclem2  26383  fdc  26386  lmclim2  26401  geomcau  26402  istotbnd  26415  isbnd  26426  prdsbnd2  26441  heiborlem6  26462  heiborlem7  26463  heiborlem8  26464  rrnval  26473  rrncmslem  26478  idlval  26560  pridlval  26580  maxidlval  26586  isnacs  26695  mzpclval  26719  mzpsubst  26742  mzprename  26743  mzpcompact2lem  26745  eldiophb  26752  diophrw  26754  eldioph2  26757  diophin  26768  diophun  26769  diophren  26811  pell1qrval  26846  pell14qrval  26848  pell1234qrval  26850  pellfundval  26880  rmxypairf1o  26911  rmxyval  26915  mzpcong  26974  pw2f1ocnv  27045  dnnumch1  27056  dfac11  27075  prdsinvgd2  27123  uvcresum  27157  frlmup1  27165  frlmup2  27166  islinds  27194  islindf5  27224  hbtlem1  27242  hbtlem7  27244  elmnc  27256  dgraaval  27264  mpaaval  27271  itgoval  27281  rgspnval  27288  flcidc  27294  psgnfval  27338  psgnval  27345  mamulid  27373  mamurid  27374  mdetleib  27403  mendval  27406  issdrg  27420  phisum  27433  mon1pid  27439  cytpval  27443  lhe4.4ex1a  27461  addrfv  27588  subrfv  27589  mulvfv  27590  itgsin0pilem1  27658  stoweidlem55  27718  wallispilem1  27728  wallispilem2  27729  wallispilem4  27731  wallispi2lem1  27734  wallispi2lem2  27735  sinhval-named  28337  coshval-named  28338  tanhval-named  28339  secval  28348  cscval  28349  cotval  28350  sgnval  28376  ceilingval  28386  lshpset  29615  lsatset  29627  lcvfbr  29657  lflset  29696  lflnegcl  29712  lkrfval  29724  lshpkrlem1  29747  lshpkrlem2  29748  lshpkrlem3  29749  ldualset  29762  cmtfvalN  29847  cvrfval  29905  pats  29922  llnset  30141  lplnset  30165  lvolset  30208  lineset  30374  pointsetN  30377  psubspset  30380  pmapfval  30392  pmapval  30393  paddfval  30433  pclfvalN  30525  polfvalN  30540  polvalN  30541  psubclsetN  30572  watfvalN  30628  watvalN  30629  lhpset  30631  lautset  30718  pautsetN  30734  ldilfset  30744  ldilset  30745  ltrnfset  30753  ltrnset  30754  dilfsetN  30788  dilsetN  30789  trnfsetN  30791  trnsetN  30792  trlfset  30796  trlset  30797  trlval  30798  tgrpfset  31380  tgrpset  31381  tendofset  31394  tendoset  31395  tendo02  31423  tendoi  31430  erngfset  31435  erngset  31436  erngfset-rN  31443  erngset-rN  31444  cdlemksv  31480  dvafset  31640  dvaset  31641  dvaplusgv  31646  diaffval  31667  diafval  31668  diaval  31669  dvhfset  31717  dvhset  31718  cdlemm10N  31755  docaffvalN  31758  docafvalN  31759  djaffvalN  31770  djafvalN  31771  dibffval  31777  dibfval  31778  dibval  31779  dicffval  31811  dicfval  31812  dicval  31813  dihffval  31867  dihfval  31868  dihval  31869  dochffval  31986  dochfval  31987  djhffval  32033  djhfval  32034  dochfl1  32113  lpolsetN  32119  lcfrlem8  32186  lcdfval  32225  lcdval  32226  mapdffval  32263  mapdfval  32264  mapdhval  32361  hvmapffval  32395  hvmapfval  32396  hdmap1ffval  32433  hdmap1fval  32434  hdmapffval  32466  hdmapfval  32467  hgmapffval  32525  hgmapfval  32526
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-iota 5409  df-fun 5447  df-fv 5453
  Copyright terms: Public domain W3C validator