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

Theorem fvmpt2 5624
Description: Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
Hypothesis
Ref Expression
fvmpt2.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
fvmpt2  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)    F( x)

Proof of Theorem fvmpt2
StepHypRef Expression
1 fvmpt2.1 . . 3  |-  F  =  ( x  e.  A  |->  B )
21fvmpt2i 5623 . 2  |-  ( x  e.  A  ->  ( F `  x )  =  (  _I  `  B
) )
3 fvi 5595 . 2  |-  ( B  e.  C  ->  (  _I  `  B )  =  B )
42, 3sylan9eq 2348 1  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    e. cmpt 4093    _I cid 4320   ` cfv 5271
This theorem is referenced by:  fvmptss  5625  fvmptdf  5627  mpteqb  5630  fvmptt  5631  fvmptf  5632  ralrnmpt  5685  fmptco  5707  f1mpt  5801  offval2  6111  ofrfval2  6112  mptelixpg  6869  dom2lem  6917  mapxpen  7043  xpmapenlem  7044  cnfcom3clem  7424  tcvalg  7439  rankf  7482  infxpenc2lem2  7663  dfac8clem  7675  acni2  7689  acnlem  7691  fin23lem32  7986  axcc2lem  8078  axcc3  8080  domtriomlem  8084  ac6num  8122  konigthlem  8206  rpnnen1lem1  10358  rpnnen1lem3  10360  rpnnen1lem5  10362  seqof  11119  rlim2  11986  ello1mpt  12011  o1compt  12077  sumrblem  12200  fsumcvg  12201  summolem2a  12204  zsum  12207  fsum  12209  fsumcvg2  12216  fsumadd  12227  isummulc2  12241  fsummulc2  12262  fsumrelem  12281  iserodd  12904  prmrec  12985  prdsbas3  13396  prdsdsval2  13399  invfuc  13864  yonedalem4c  14067  gsumconst  15225  prdsgsum  15245  dprdwd  15262  gsumdixp  15408  evlslem4  16261  elptr2  17285  ptunimpt  17306  ptcldmpt  17324  ptclsg  17325  txcnp  17330  ptcnplem  17331  cnmpt11  17373  cnmpt1t  17375  cnmptk2  17396  xkocnv  17521  flfcnp2  17718  iccpnfcnv  18458  ovolctb  18865  ovoliunlem1  18877  ovoliun2  18881  ovolshftlem1  18884  ovolscalem1  18888  voliun  18927  ioombl1lem3  18933  ioombl1lem4  18934  uniioombllem2  18954  mbfeqalem  19013  mbfpos  19022  mbfposr  19023  mbfposb  19024  mbfsup  19035  mbfinf  19036  mbflim  19039  i1fposd  19078  itg1climres  19085  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  itg2split  19120  itg2mono  19124  itg2cnlem1  19132  isibl2  19137  itgmpt  19153  itgeqa  19184  itggt0  19212  itgcn  19213  limcmpt  19249  dvlipcn  19357  lhop2  19378  dvfsumabs  19386  itgparts  19410  itgsubstlem  19411  itgsubst  19412  elplyd  19600  coeeulem  19622  coeeq2  19640  dvply1  19680  plyremlem  19700  ulmss  19790  ulmdvlem1  19793  mtest  19797  itgulm2  19801  radcnvlem1  19805  pserulm  19814  leibpi  20254  rlimcnp  20276  o1cxp  20285  sqff1o  20436  lgseisenlem2  20605  dchrvmasumlem1  20660  ubthlem1  21465  cnlnadjlem5  22667  xppreima2  23227  abfmpunirn  23231  fvmpt2d  23240  xrmulc1cn  23318  esumpcvgval  23461  iscvm  23805  prodrblem  24152  fprodcvg  24153  prodmolem2a  24157  zprod  24160  fprod  24164  itggt0cn  25023  fprodadd  25455  fprodneg  25481  fprodsub  25482  trooo  25497  trinv  25498  ltrinvlem  25509  rltrooo  25518  svli2  25587  trnij  25718  cnegvex2  25763  rnegvex2  25764  mulmulvec  25790  distmlva  25791  distsava  25792  elrfirn2  26874  eq0rabdioph  26959  monotoddzz  27131  aomclem2  27255  refsumcn  27804  refsum2cnlem1  27811  fmuldfeqlem1  27815  fmuldfeq  27816  climneg  27839  climdivf  27841  itgsin0pilem1  27847  ibliccsinexp  27848  itgsinexplem1  27851  itgsinexp  27852  stoweidlem2  27854  stoweidlem11  27863  stoweidlem12  27864  stoweidlem16  27868  stoweidlem17  27869  stoweidlem18  27870  stoweidlem19  27871  stoweidlem20  27872  stoweidlem21  27873  stoweidlem22  27874  stoweidlem23  27875  stoweidlem27  27879  stoweidlem31  27883  stoweidlem34  27886  stoweidlem36  27888  stoweidlem40  27892  stoweidlem41  27893  stoweidlem42  27894  stoweidlem48  27900  stoweidlem51  27903  stoweidlem55  27907  stoweidlem59  27911  stoweidlem62  27914  stirlinglem3  27928  stirlinglem8  27933  stirlinglem14  27939  stirlinglem15  27940  stirlingr  27942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fv 5279
  Copyright terms: Public domain W3C validator