Theorem fvmpt2 5944

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

Step	Hyp	Ref	Expression
1		fvmpt2.1	. . 3 |- F = ( x e. A |-> B )
2	1	fvmpt2i 5943	. 2 |- ( x e. A -> ( F ` x ) = ( _I ` B ) )
3		fvi 5911	. 2 |- ( B e. C -> ( _I ` B ) = B )
4	2, 3	sylan9eq 2502	1 |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1381   e. wcel 1802   |-> cmpt 4491   _I cid 4776   ` cfv 5574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fv 5582

This theorem is referenced by:  fvmptss  5945  fvmpt2d  5946  fvmptdf  5948  mpteqb  5951  fvmptt  5952  fvmptf  5953  fnmptfvd  5971  ralrnmpt  6021  fmptco  6045  f1mpt  6150  offval2  6537  ofrfval2  6538  mptelixpg  7504  dom2lem  7553  mapxpen  7681  xpmapenlem  7682  cnfcom3clem  8147  cnfcom3clemOLD  8155  tcvalg  8167  rankf  8210  infxpenc2lem2  8395  infxpenc2lem2OLD  8399  dfac8clem  8411  acni2  8425  acnlem  8427  fin23lem32  8722  axcc2lem  8814  axcc3  8816  domtriomlem  8820  ac6num  8857  konigthlem  8941  rpnnen1lem1  11212  rpnnen1lem3  11214  rpnnen1lem5  11216  seqof  12138  seqof2  12139  rlim2  13293  ello1mpt  13318  o1compt  13384  sumrblem  13507  fsumcvg  13508  summolem2a  13511  fsum  13516  fsumcvg2  13523  fsumadd  13535  isummulc2  13551  fsummulc2  13573  fsumrelem  13595  iserodd  14231  prmrec  14312  prdsbas3  14750  prdsdsval2  14753  invfuc  15212  yonedalem4c  15415  gsumconst  16823  prdsgsum  16876  prdsgsumOLD  16877  dprdwd  16913  dprdwdOLD  16919  gsumdixpOLD  17125  gsumdixp  17126  evlslem4OLD  18041  evlslem4  18042  elptr2  19941  ptunimpt  19962  ptcldmpt  19981  ptclsg  19982  txcnp  19987  ptcnplem  19988  cnmpt11  20030  cnmpt1t  20032  cnmptk2  20053  xkocnv  20181  flfcnp2  20374  ustn0  20589  utopsnneiplem  20616  ucnima  20650  iccpnfcnv  21310  ovolctb  21767  ovoliunlem1  21779  ovoliun2  21783  ovolshftlem1  21786  ovolscalem1  21790  voliun  21830  ioombl1lem3  21836  ioombl1lem4  21837  uniioombllem2  21858  mbfeqalem  21915  mbfpos  21924  mbfposr  21925  mbfposb  21926  mbfsup  21937  mbfinf  21938  mbflim  21941  i1fposd  21980  itg1climres  21987  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  mbfi1fseqlem6  21993  itg2split  22022  itg2mono  22026  itg2cnlem1  22034  isibl2  22039  itgmpt  22055  itgeqa  22086  itggt0  22114  itgcn  22115  limcmpt  22153  dvlipcn  22261  lhop2  22282  dvfsumabs  22290  itgparts  22314  itgsubstlem  22315  itgsubst  22316  elplyd  22465  coeeulem  22487  coeeq2  22505  dvply1  22545  plyremlem  22565  ulmss  22657  ulmdvlem1  22660  mtest  22664  itgulm2  22669  radcnvlem1  22673  pserulm  22682  leibpi  23138  rlimcnp  23160  o1cxp  23169  sqff1o  23321  lgseisenlem2  23490  dchrvmasumlem1  23545  frgrancvvdeqlem6  24900  ubthlem1  25651  cnlnadjlem5  26855  xppreima2  27353  abfmpunirn  27355  fpwrelmap  27421  fimaproj  27702  xrmulc1cn  27778  esumpcvgval  27950  voliune  28067  eulerpartgbij  28177  signsplypnf  28373  lgamgulmlem2  28438  lgamgulmlem6  28442  lgamgulm2  28444  iscvm  28570  mclsrcl  28787  prodrblem  29029  fprodcvg  29030  prodmolem2a  29034  zprod  29037  fprod  29041  fprodmul  29058  fproddiv  29059  itg2addnclem  30034  itggt0cn  30055  ftc1anclem5  30062  elrfirn2  30596  eq0rabdioph  30678  monotoddzz  30847  aomclem2  30969  refsumcn  31352  refsum2cnlem1  31359  fvmpt2bd  31392  fmuldfeqlem1  31500  fmuldfeq  31501  climneg  31520  climdivf  31522  mullimc  31526  idlimc  31536  sumnnodd  31540  neglimc  31557  addlimc  31558  0ellimcdiv  31559  cncfmptssg  31575  cncfshift  31579  icccncfext  31593  cncfiooicclem1  31599  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  itgsin0pilem1  31634  ibliccsinexp  31635  itgsinexplem1  31638  itgsinexp  31639  ditgeqiooicc  31645  itgsubsticclem  31660  itgioocnicc  31662  stoweidlem2  31669  stoweidlem11  31678  stoweidlem12  31679  stoweidlem16  31683  stoweidlem17  31684  stoweidlem18  31685  stoweidlem19  31686  stoweidlem20  31687  stoweidlem21  31688  stoweidlem22  31689  stoweidlem23  31690  stoweidlem27  31694  stoweidlem31  31698  stoweidlem34  31701  stoweidlem36  31703  stoweidlem40  31707  stoweidlem41  31708  stoweidlem42  31709  stoweidlem48  31715  stoweidlem55  31722  stoweidlem59  31726  stoweidlem62  31729  stirlinglem3  31743  stirlinglem8  31748  stirlinglem14  31754  stirlinglem15  31755  stirlingr  31757  dirkeritg  31769  dirkercncflem2  31771  fourierdlem14  31788  fourierdlem31  31805  fourierdlem41  31815  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem51  31825  fourierdlem56  31830  fourierdlem60  31834  fourierdlem61  31835  fourierdlem66  31840  fourierdlem70  31844  fourierdlem71  31845  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem77  31851  fourierdlem78  31852  fourierdlem81  31855  fourierdlem83  31857  fourierdlem84  31858  fourierdlem85  31859  fourierdlem87  31861  fourierdlem88  31862  fourierdlem89  31863  fourierdlem91  31865  fourierdlem92  31866  fourierdlem93  31867  fourierdlem95  31869  fourierdlem97  31871  fourierdlem101  31875  fourierdlem103  31877  fourierdlem104  31878  fourierdlem111  31885  fourierdlem112  31886  sqwvfoura  31896  sqwvfourb  31897  fouriersw  31899