Theorem fvmpt2 5964

Description: Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)

Hypothesis

Ref	Expression
mptrcl.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

Step	Hyp	Ref	Expression
1		mptrcl.1	. . 3 |- F = ( x e. A |-> B )
2	1	fvmpt2i 5963	. 2 |- ( x e. A -> ( F ` x ) = ( _I ` B ) )
3		fvi 5929	. 2 |- ( B e. C -> ( _I ` B ) = B )
4	2, 3	sylan9eq 2481	1 |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1867   |-> cmpt 4475   _I cid 4755   ` cfv 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fv 5600

This theorem is referenced by:  fvmptss  5965  fvmpt2d  5966  fvmptdf  5968  mpteqb  5971  fvmptt  5972  fvmptf  5973  fnmptfvd  5991  ralrnmpt  6037  fmptco  6062  f1mpt  6168  offval2  6553  ofrfval2  6554  mptelixpg  7558  dom2lem  7607  mapxpen  7735  xpmapenlem  7736  cnfcom3clem  8200  tcvalg  8212  rankf  8255  infxpenc2lem2  8440  dfac8clem  8452  acni2  8466  acnlem  8468  fin23lem32  8763  axcc2lem  8855  axcc3  8857  domtriomlem  8861  ac6num  8898  konigthlem  8982  rpnnen1lem1  11279  rpnnen1lem3  11281  rpnnen1lem5  11283  seqof  12256  seqof2  12257  rlim2  13527  ello1mpt  13552  o1compt  13618  sumrblem  13744  fsumcvg  13745  summolem2a  13748  fsum  13753  fsumcvg2  13760  fsumadd  13772  isummulc2  13790  fsummulc2  13812  fsumrelem  13834  prodrblem  13950  fprodcvg  13951  prodmolem2a  13955  zprod  13958  fprod  13962  fprodmul  13981  fproddiv  13982  iserodd  14737  prmrec  14818  prdsbas3  15331  prdsdsval2  15334  invfuc  15823  yonedalem4c  16106  gsumconst  17495  prdsgsum  17538  dprdwdOLD  17572  gsumdixp  17765  evlslem4  18659  elptr2  20513  ptunimpt  20534  ptcldmpt  20553  ptclsg  20554  txcnp  20559  ptcnplem  20560  cnmpt11  20602  cnmpt1t  20604  cnmptk2  20625  xkocnv  20753  flfcnp2  20946  ustn0  21159  utopsnneiplem  21186  ucnima  21220  iccpnfcnv  21861  ovolctb  22317  ovoliunlem1  22329  ovoliun2  22333  ovolshftlem1  22336  ovolscalem1  22340  voliun  22381  ioombl1lem3  22387  ioombl1lem4  22388  uniioombllem2  22414  uniioombllem2OLD  22415  mbfeqalem  22472  mbfpos  22481  mbfposr  22482  mbfposb  22483  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  mbflim  22500  i1fposd  22539  itg1climres  22546  mbfi1fseqlem4  22550  mbfi1fseqlem5  22551  mbfi1fseqlem6  22552  itg2split  22581  itg2mono  22585  itg2cnlem1  22593  isibl2  22598  itgmpt  22614  itgeqa  22645  itggt0  22673  itgcn  22674  limcmpt  22712  dvlipcn  22820  lhop2  22841  dvfsumabs  22849  itgparts  22873  itgsubstlem  22874  itgsubst  22875  elplyd  23021  coeeulem  23043  coeeq2  23061  dvply1  23102  plyremlem  23122  ulmss  23214  ulmdvlem1  23217  mtest  23221  itgulm2  23226  radcnvlem1  23230  pserulm  23239  leibpi  23730  rlimcnp  23753  o1cxp  23762  lgamgulmlem2  23817  lgamgulmlem6  23821  lgamgulm2  23823  sqff1o  23969  lgseisenlem2  24138  dchrvmasumlem1  24193  frgrancvvdeqlem6  25605  ubthlem1  26354  cnlnadjlem5  27556  xppreima2  28086  abfmpunirn  28088  aciunf1lem  28101  fpwrelmap  28158  fimaproj  28496  xrmulc1cn  28572  esumpcvgval  28735  esumsup  28746  voliune  28888  eulerpartgbij  29028  signsplypnf  29224  iscvm  29767  mclsrcl  29984  f1omptsnlem  31469  itg2addnclem  31697  itggt0cn  31718  ftc1anclem5  31725  elrfirn2  35247  eq0rabdioph  35328  monotoddzz  35501  aomclem2  35623  refsumcn  36995  refsum2cnlem1  37002  fvmpt2bd  37060  wessf1ornlem  37086  fompt  37094  fmuldfeqlem1  37236  fmuldfeq  37237  climneg  37265  climdivf  37268  mullimc  37272  idlimc  37282  sumnnodd  37286  neglimc  37304  addlimc  37305  0ellimcdiv  37306  cncfmptssg  37323  cncfshift  37327  icccncfext  37341  cncfiooicclem1  37347  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnmptdivc  37386  dvnmul  37391  dvnprodlem2  37395  itgsin0pilem1  37399  ibliccsinexp  37400  itgsinexplem1  37403  itgsinexp  37404  ditgeqiooicc  37410  itgsubsticclem  37425  itgioocnicc  37427  stoweidlem2  37435  stoweidlem11  37444  stoweidlem12  37445  stoweidlem16  37449  stoweidlem17  37450  stoweidlem18  37451  stoweidlem19  37452  stoweidlem20  37453  stoweidlem21  37454  stoweidlem22  37455  stoweidlem23  37456  stoweidlem27  37460  stoweidlem31  37465  stoweidlem34  37468  stoweidlem36  37470  stoweidlem40  37474  stoweidlem41  37475  stoweidlem42  37476  stoweidlem48  37482  stoweidlem55  37489  stoweidlem59  37493  stoweidlem62  37496  stoweidlem62OLD  37497  stirlinglem3  37511  stirlinglem8  37516  stirlinglem14  37522  stirlinglem15  37523  stirlingr  37525  dirkeritg  37537  dirkercncflem2  37539  fourierdlem14  37556  fourierdlem31  37573  fourierdlem41  37583  fourierdlem48  37590  fourierdlem49  37591  fourierdlem50  37592  fourierdlem51  37593  fourierdlem56  37598  fourierdlem60  37602  fourierdlem61  37603  fourierdlem66  37608  fourierdlem70  37612  fourierdlem71  37613  fourierdlem73  37615  fourierdlem74  37616  fourierdlem75  37617  fourierdlem76  37618  fourierdlem77  37619  fourierdlem78  37620  fourierdlem81  37623  fourierdlem83  37625  fourierdlem84  37626  fourierdlem85  37627  fourierdlem87  37629  fourierdlem88  37630  fourierdlem89  37631  fourierdlem91  37633  fourierdlem92  37634  fourierdlem93  37635  fourierdlem95  37637  fourierdlem97  37639  fourierdlem101  37643  fourierdlem103  37645  fourierdlem104  37646  fourierdlem111  37653  fourierdlem112  37654  sqwvfoura  37664  sqwvfourb  37665  fouriersw  37667  elaa2lem  37669  etransclem4  37674  etransclem13  37683  etransclem35  37705  etransclem46  37716  etransclem48  37718  sge0revalmpt  37758  sge0fsummpt  37770  sge0iunmptlemfi  37793  sge0iunmptlemre  37795  nnfoctbdjlem  37806  iundjiun  37811  meaiunlelem  37819  omeiunlempt  37854  carageniuncllem2  37856  caratheodorylem2  37861  aacllem  39314