Theorem fvmpt2 5769

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   e. cmpt 4338   _I cid 4618   ` cfv 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fv 5414

This theorem is referenced by:  fvmptss  5770  fvmpt2d  5771  fvmptdf  5773  mpteqb  5776  fvmptt  5777  fvmptf  5778  fnmptfvd  5794  ralrnmpt  5840  fmptco  5863  f1mpt  5961  offval2  6325  ofrfval2  6326  mptelixpg  7288  dom2lem  7337  mapxpen  7465  xpmapenlem  7466  cnfcom3clem  7926  cnfcom3clemOLD  7934  tcvalg  7946  rankf  7989  infxpenc2lem2  8174  infxpenc2lem2OLD  8178  dfac8clem  8190  acni2  8204  acnlem  8206  fin23lem32  8501  axcc2lem  8593  axcc3  8595  domtriomlem  8599  ac6num  8636  konigthlem  8720  rpnnen1lem1  10966  rpnnen1lem3  10968  rpnnen1lem5  10970  seqof  11846  seqof2  11847  rlim2  12957  ello1mpt  12982  o1compt  13048  sumrblem  13171  fsumcvg  13172  summolem2a  13175  fsum  13180  fsumcvg2  13187  fsumadd  13198  isummulc2  13212  fsummulc2  13233  fsumrelem  13252  iserodd  13884  prmrec  13965  prdsbas3  14401  prdsdsval2  14404  invfuc  14866  yonedalem4c  15069  gsumconst  16405  prdsgsum  16444  prdsgsumOLD  16445  dprdwd  16468  dprdwdOLD  16474  gsumdixpOLD  16634  gsumdixp  16635  evlslem4OLD  17517  evlslem4  17518  elptr2  18988  ptunimpt  19009  ptcldmpt  19028  ptclsg  19029  txcnp  19034  ptcnplem  19035  cnmpt11  19077  cnmpt1t  19079  cnmptk2  19100  xkocnv  19228  flfcnp2  19421  ustn0  19636  utopsnneiplem  19663  ucnima  19697  iccpnfcnv  20357  ovolctb  20814  ovoliunlem1  20826  ovoliun2  20830  ovolshftlem1  20833  ovolscalem1  20837  voliun  20876  ioombl1lem3  20882  ioombl1lem4  20883  uniioombllem2  20904  mbfeqalem  20961  mbfpos  20970  mbfposr  20971  mbfposb  20972  mbfsup  20983  mbfinf  20984  mbflim  20987  i1fposd  21026  itg1climres  21033  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1fseqlem6  21039  itg2split  21068  itg2mono  21072  itg2cnlem1  21080  isibl2  21085  itgmpt  21101  itgeqa  21132  itggt0  21160  itgcn  21161  limcmpt  21199  dvlipcn  21307  lhop2  21328  dvfsumabs  21336  itgparts  21360  itgsubstlem  21361  itgsubst  21362  elplyd  21554  coeeulem  21576  coeeq2  21594  dvply1  21634  plyremlem  21654  ulmss  21746  ulmdvlem1  21749  mtest  21753  itgulm2  21758  radcnvlem1  21762  pserulm  21771  leibpi  22221  rlimcnp  22243  o1cxp  22252  sqff1o  22404  lgseisenlem2  22573  dchrvmasumlem1  22628  ubthlem1  24093  cnlnadjlem5  25297  xppreima2  25788  abfmpunirn  25790  fpwrelmap  25857  xrmulc1cn  26213  esumpcvgval  26380  voliune  26498  eulerpartgbij  26602  signsplypnf  26798  lgamgulmlem2  26863  lgamgulmlem6  26867  lgamgulm2  26869  iscvm  26995  prodrblem  27288  fprodcvg  27289  prodmolem2a  27293  zprod  27296  fprod  27300  fprodmul  27317  fproddiv  27318  itg2addnclem  28284  itggt0cn  28305  ftc1anclem5  28312  elrfirn2  28874  eq0rabdioph  28957  monotoddzz  29126  aomclem2  29250  refsumcn  29594  refsum2cnlem1  29601  fmuldfeqlem1  29605  fmuldfeq  29606  climneg  29626  climdivf  29628  itgsin0pilem1  29633  ibliccsinexp  29634  itgsinexplem1  29637  itgsinexp  29638  stoweidlem2  29640  stoweidlem11  29649  stoweidlem12  29650  stoweidlem16  29654  stoweidlem17  29655  stoweidlem18  29656  stoweidlem19  29657  stoweidlem20  29658  stoweidlem21  29659  stoweidlem22  29660  stoweidlem23  29661  stoweidlem27  29665  stoweidlem31  29669  stoweidlem34  29672  stoweidlem36  29674  stoweidlem40  29678  stoweidlem41  29679  stoweidlem42  29680  stoweidlem48  29686  stoweidlem55  29693  stoweidlem59  29697  stoweidlem62  29700  stirlinglem3  29714  stirlinglem8  29719  stirlinglem14  29725  stirlinglem15  29726  stirlingr  29728  frgrancvvdeqlem6  30471