Theorem fvmpt2 5957

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 5956	. 2 |- ( x e. A -> ( F ` x ) = ( _I ` B ) )
3		fvi 5924	. 2 |- ( B e. C -> ( _I ` B ) = B )
4	2, 3	sylan9eq 2528	1 |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   |-> cmpt 4505   _I cid 4790   ` cfv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fv 5596

This theorem is referenced by:  fvmptss  5958  fvmpt2d  5959  fvmptdf  5961  mpteqb  5964  fvmptt  5965  fvmptf  5966  fnmptfvd  5984  ralrnmpt  6030  fmptco  6054  f1mpt  6157  offval2  6540  ofrfval2  6541  mptelixpg  7506  dom2lem  7555  mapxpen  7683  xpmapenlem  7684  cnfcom3clem  8149  cnfcom3clemOLD  8157  tcvalg  8169  rankf  8212  infxpenc2lem2  8397  infxpenc2lem2OLD  8401  dfac8clem  8413  acni2  8427  acnlem  8429  fin23lem32  8724  axcc2lem  8816  axcc3  8818  domtriomlem  8822  ac6num  8859  konigthlem  8943  rpnnen1lem1  11208  rpnnen1lem3  11210  rpnnen1lem5  11212  seqof  12132  seqof2  12133  rlim2  13282  ello1mpt  13307  o1compt  13373  sumrblem  13496  fsumcvg  13497  summolem2a  13500  fsum  13505  fsumcvg2  13512  fsumadd  13524  isummulc2  13540  fsummulc2  13562  fsumrelem  13584  iserodd  14218  prmrec  14299  prdsbas3  14736  prdsdsval2  14739  invfuc  15201  yonedalem4c  15404  gsumconst  16757  prdsgsum  16810  prdsgsumOLD  16811  dprdwd  16847  dprdwdOLD  16853  gsumdixpOLD  17058  gsumdixp  17059  evlslem4OLD  17972  evlslem4  17973  elptr2  19838  ptunimpt  19859  ptcldmpt  19878  ptclsg  19879  txcnp  19884  ptcnplem  19885  cnmpt11  19927  cnmpt1t  19929  cnmptk2  19950  xkocnv  20078  flfcnp2  20271  ustn0  20486  utopsnneiplem  20513  ucnima  20547  iccpnfcnv  21207  ovolctb  21664  ovoliunlem1  21676  ovoliun2  21680  ovolshftlem1  21683  ovolscalem1  21687  voliun  21727  ioombl1lem3  21733  ioombl1lem4  21734  uniioombllem2  21755  mbfeqalem  21812  mbfpos  21821  mbfposr  21822  mbfposb  21823  mbfsup  21834  mbfinf  21835  mbflim  21838  i1fposd  21877  itg1climres  21884  mbfi1fseqlem4  21888  mbfi1fseqlem5  21889  mbfi1fseqlem6  21890  itg2split  21919  itg2mono  21923  itg2cnlem1  21931  isibl2  21936  itgmpt  21952  itgeqa  21983  itggt0  22011  itgcn  22012  limcmpt  22050  dvlipcn  22158  lhop2  22179  dvfsumabs  22187  itgparts  22211  itgsubstlem  22212  itgsubst  22213  elplyd  22362  coeeulem  22384  coeeq2  22402  dvply1  22442  plyremlem  22462  ulmss  22554  ulmdvlem1  22557  mtest  22561  itgulm2  22566  radcnvlem1  22570  pserulm  22579  leibpi  23029  rlimcnp  23051  o1cxp  23060  sqff1o  23212  lgseisenlem2  23381  dchrvmasumlem1  23436  frgrancvvdeqlem6  24740  ubthlem1  25490  cnlnadjlem5  26694  xppreima2  27188  abfmpunirn  27190  fpwrelmap  27256  fimaproj  27527  xrmulc1cn  27576  esumpcvgval  27752  voliune  27869  eulerpartgbij  27979  signsplypnf  28175  lgamgulmlem2  28240  lgamgulmlem6  28244  lgamgulm2  28246  iscvm  28372  prodrblem  28666  fprodcvg  28667  prodmolem2a  28671  zprod  28674  fprod  28678  fprodmul  28695  fproddiv  28696  itg2addnclem  29671  itggt0cn  29692  ftc1anclem5  29699  elrfirn2  30260  eq0rabdioph  30342  monotoddzz  30511  aomclem2  30633  refsumcn  31011  refsum2cnlem1  31018  fvmpt2bd  31052  fmuldfeqlem1  31160  fmuldfeq  31161  climneg  31180  climdivf  31182  mullimc  31186  idlimc  31196  sumnnodd  31200  neglimc  31217  addlimc  31218  0ellimcdiv  31219  cncfmptssg  31236  cncfshift  31240  icccncfext  31254  cncficcgt0  31255  cncfiooicclem1  31260  dvdivbd  31281  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  itgsin0pilem1  31295  ibliccsinexp  31296  itgsinexplem1  31299  itgsinexp  31300  ditgeqiooicc  31306  itgsubsticclem  31321  itgioocnicc  31323  stoweidlem2  31330  stoweidlem11  31339  stoweidlem12  31340  stoweidlem16  31344  stoweidlem17  31345  stoweidlem18  31346  stoweidlem19  31347  stoweidlem20  31348  stoweidlem21  31349  stoweidlem22  31350  stoweidlem23  31351  stoweidlem27  31355  stoweidlem31  31359  stoweidlem34  31362  stoweidlem36  31364  stoweidlem40  31368  stoweidlem41  31369  stoweidlem42  31370  stoweidlem48  31376  stoweidlem55  31383  stoweidlem59  31387  stoweidlem62  31390  stirlinglem3  31404  stirlinglem8  31409  stirlinglem14  31415  stirlinglem15  31416  stirlingr  31418  dirkeritg  31430  dirkercncflem2  31432  fourierdlem14  31449  fourierdlem31  31466  fourierdlem41  31476  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem51  31486  fourierdlem56  31491  fourierdlem60  31495  fourierdlem61  31496  fourierdlem66  31501  fourierdlem70  31505  fourierdlem71  31506  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem77  31512  fourierdlem78  31513  fourierdlem81  31516  fourierdlem83  31518  fourierdlem84  31519  fourierdlem85  31520  fourierdlem87  31522  fourierdlem88  31523  fourierdlem89  31524  fourierdlem91  31526  fourierdlem92  31527  fourierdlem93  31528  fourierdlem95  31530  fourierdlem97  31532  fourierdlem101  31536  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fourierdlem112  31547  sqwvfoura  31557  sqwvfourb  31558  fouriersw  31560