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

Theorem fvmpt2 5569
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 5568 . 2  |-  ( x  e.  A  ->  ( F `  x )  =  (  _I  `  B
) )
3 fvi 5540 . 2  |-  ( B  e.  C  ->  (  _I  `  B )  =  B )
42, 3sylan9eq 2336 1  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685    e. cmpt 4078    _I cid 4303   ` cfv 5221
This theorem is referenced by:  fvmptss  5570  fvmptdf  5572  mpteqb  5575  fvmptt  5576  fvmptf  5577  ralrnmpt  5630  fmptco  5652  f1mpt  5746  offval2  6056  ofrfval2  6057  mptelixpg  6848  dom2lem  6896  mapxpen  7022  xpmapenlem  7023  cnfcom3clem  7403  tcvalg  7418  rankf  7461  infxpenc2lem2  7642  dfac8clem  7654  acni2  7668  acnlem  7670  fin23lem32  7965  axcc2lem  8057  axcc3  8059  domtriomlem  8063  ac6num  8101  konigthlem  8185  rpnnen1lem1  10337  rpnnen1lem3  10339  rpnnen1lem5  10341  seqof  11097  rlim2  11964  ello1mpt  11989  o1compt  12055  sumrblem  12178  fsumcvg  12179  summolem2a  12182  zsum  12185  fsum  12187  fsumcvg2  12194  fsumadd  12205  isummulc2  12219  fsummulc2  12240  fsumrelem  12259  iserodd  12882  prmrec  12963  prdsbas3  13374  prdsdsval2  13377  invfuc  13842  yonedalem4c  14045  gsumconst  15203  prdsgsum  15223  dprdwd  15240  gsumdixp  15386  evlslem4  16239  elptr2  17263  ptunimpt  17284  ptcldmpt  17302  ptclsg  17303  txcnp  17308  ptcnplem  17309  cnmpt11  17351  cnmpt1t  17353  cnmptk2  17374  xkocnv  17499  flfcnp2  17696  iccpnfcnv  18436  ovolctb  18843  ovoliunlem1  18855  ovoliun2  18859  ovolshftlem1  18862  ovolscalem1  18866  voliun  18905  ioombl1lem3  18911  ioombl1lem4  18912  uniioombllem2  18932  mbfeqalem  18991  mbfpos  19000  mbfposr  19001  mbfposb  19002  mbfsup  19013  mbfinf  19014  mbflim  19017  i1fposd  19056  itg1climres  19063  mbfi1fseqlem4  19067  mbfi1fseqlem5  19068  mbfi1fseqlem6  19069  itg2split  19098  itg2mono  19102  itg2cnlem1  19110  isibl2  19115  itgmpt  19131  itgeqa  19162  itggt0  19190  itgcn  19191  limcmpt  19227  dvlipcn  19335  lhop2  19356  dvfsumabs  19364  itgparts  19388  itgsubstlem  19389  itgsubst  19390  elplyd  19578  coeeulem  19600  coeeq2  19618  dvply1  19658  plyremlem  19678  ulmss  19768  ulmdvlem1  19771  mtest  19775  itgulm2  19779  radcnvlem1  19783  pserulm  19792  leibpi  20232  rlimcnp  20254  o1cxp  20263  sqff1o  20414  lgseisenlem2  20583  dchrvmasumlem1  20638  ubthlem1  21441  cnlnadjlem5  22643  iscvm  23194  fprodadd  24751  fprodneg  24777  fprodsub  24778  trooo  24793  trinv  24794  ltrinvlem  24805  rltrooo  24814  svli2  24883  trnij  25014  cnegvex2  25059  rnegvex2  25060  mulmulvec  25086  distmlva  25087  distsava  25088  elrfirn2  26170  eq0rabdioph  26255  monotoddzz  26427  aomclem2  26551  refsumcn  27100  refsum2cnlem1  27107  fmuldfeqlem1  27111  fmuldfeq  27112  climneg  27135  climdivf  27137  itgsin0pilem1  27143  ibliccsinexp  27144  itgsinexplem1  27147  itgsinexp  27148  stoweidlem2  27150  stoweidlem11  27159  stoweidlem12  27160  stoweidlem16  27164  stoweidlem17  27165  stoweidlem18  27166  stoweidlem19  27167  stoweidlem20  27168  stoweidlem21  27169  stoweidlem22  27170  stoweidlem23  27171  stoweidlem27  27175  stoweidlem31  27179  stoweidlem34  27182  stoweidlem36  27184  stoweidlem40  27188  stoweidlem41  27189  stoweidlem42  27190  stoweidlem48  27196  stoweidlem51  27199  stoweidlem55  27203  stoweidlem59  27207  stoweidlem62  27210  stirlinglem3  27224  stirlinglem8  27229  stirlinglem14  27235  stirlinglem15  27236  stirlingr  27238
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fv 5229
  Copyright terms: Public domain W3C validator