Theorem fvmpt2 5771

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

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   e. cmpt 4226   _I cid 4453   ` cfv 5413

This theorem is referenced by:  fvmptss  5772  fvmpt2d  5773  fvmptdf  5775  mpteqb  5778  fvmptt  5779  fvmptf  5780  ralrnmpt  5837  fmptco  5860  f1mpt  5966  offval2  6281  ofrfval2  6282  mptelixpg  7058  dom2lem  7106  mapxpen  7232  xpmapenlem  7233  cnfcom3clem  7618  tcvalg  7633  rankf  7676  infxpenc2lem2  7857  dfac8clem  7869  acni2  7883  acnlem  7885  fin23lem32  8180  axcc2lem  8272  axcc3  8274  domtriomlem  8278  ac6num  8315  konigthlem  8399  rpnnen1lem1  10556  rpnnen1lem3  10558  rpnnen1lem5  10560  seqof  11335  seqof2  11336  rlim2  12245  ello1mpt  12270  o1compt  12336  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  fsum  12469  fsumcvg2  12476  fsumadd  12487  isummulc2  12501  fsummulc2  12522  fsumrelem  12541  iserodd  13164  prmrec  13245  prdsbas3  13658  prdsdsval2  13661  invfuc  14126  yonedalem4c  14329  gsumconst  15487  prdsgsum  15507  dprdwd  15524  gsumdixp  15670  evlslem4  16519  elptr2  17559  ptunimpt  17580  ptcldmpt  17599  ptclsg  17600  txcnp  17605  ptcnplem  17606  cnmpt11  17648  cnmpt1t  17650  cnmptk2  17671  xkocnv  17799  flfcnp2  17992  ustn0  18203  utopsnneiplem  18230  ucnima  18264  iccpnfcnv  18922  ovolctb  19339  ovoliunlem1  19351  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  voliun  19401  ioombl1lem3  19407  ioombl1lem4  19408  uniioombllem2  19428  mbfeqalem  19487  mbfpos  19496  mbfposr  19497  mbfposb  19498  mbfsup  19509  mbfinf  19510  mbflim  19513  i1fposd  19552  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2split  19594  itg2mono  19598  itg2cnlem1  19606  isibl2  19611  itgmpt  19627  itgeqa  19658  itggt0  19686  itgcn  19687  limcmpt  19723  dvlipcn  19831  lhop2  19852  dvfsumabs  19860  itgparts  19884  itgsubstlem  19885  itgsubst  19886  elplyd  20074  coeeulem  20096  coeeq2  20114  dvply1  20154  plyremlem  20174  ulmss  20266  ulmdvlem1  20269  mtest  20273  itgulm2  20278  radcnvlem1  20282  pserulm  20291  leibpi  20735  rlimcnp  20757  o1cxp  20766  sqff1o  20918  lgseisenlem2  21087  dchrvmasumlem1  21142  ubthlem1  22325  cnlnadjlem5  23527  xppreima2  24013  abfmpunirn  24017  xrmulc1cn  24269  esumpcvgval  24421  voliune  24538  lgamgulmlem2  24767  lgamgulmlem6  24771  lgamgulm2  24773  iscvm  24899  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  fprod  25220  fprodmul  25237  fproddiv  25238  itg2addnclem  26155  itggt0cn  26176  elrfirn2  26640  eq0rabdioph  26725  monotoddzz  26896  aomclem2  27020  refsumcn  27568  refsum2cnlem1  27575  fmuldfeqlem1  27579  fmuldfeq  27580  climneg  27603  climdivf  27605  itgsin0pilem1  27611  ibliccsinexp  27612  itgsinexplem1  27615  itgsinexp  27616  stoweidlem2  27618  stoweidlem11  27627  stoweidlem12  27628  stoweidlem16  27632  stoweidlem17  27633  stoweidlem18  27634  stoweidlem19  27635  stoweidlem20  27636  stoweidlem21  27637  stoweidlem22  27638  stoweidlem23  27639  stoweidlem27  27643  stoweidlem31  27647  stoweidlem34  27650  stoweidlem36  27652  stoweidlem40  27656  stoweidlem41  27657  stoweidlem42  27658  stoweidlem48  27664  stoweidlem55  27671  stoweidlem59  27675  stoweidlem62  27678  stirlinglem3  27692  stirlinglem8  27697  stirlinglem14  27703  stirlinglem15  27704  stirlingr  27706  frgrancvvdeqlem6  28138

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fv 5421