Theorem fvmpt2 5802

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   e. cmpt 4371   _I cid 4652   ` cfv 5439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fv 5447

This theorem is referenced by:  fvmptss  5803  fvmpt2d  5804  fvmptdf  5806  mpteqb  5809  fvmptt  5810  fvmptf  5811  fnmptfvd  5827  ralrnmpt  5873  fmptco  5897  f1mpt  5995  offval2  6357  ofrfval2  6358  mptelixpg  7321  dom2lem  7370  mapxpen  7498  xpmapenlem  7499  cnfcom3clem  7959  cnfcom3clemOLD  7967  tcvalg  7979  rankf  8022  infxpenc2lem2  8207  infxpenc2lem2OLD  8211  dfac8clem  8223  acni2  8237  acnlem  8239  fin23lem32  8534  axcc2lem  8626  axcc3  8628  domtriomlem  8632  ac6num  8669  konigthlem  8753  rpnnen1lem1  11000  rpnnen1lem3  11002  rpnnen1lem5  11004  seqof  11884  seqof2  11885  rlim2  12995  ello1mpt  13020  o1compt  13086  sumrblem  13209  fsumcvg  13210  summolem2a  13213  fsum  13218  fsumcvg2  13225  fsumadd  13236  isummulc2  13250  fsummulc2  13272  fsumrelem  13291  iserodd  13923  prmrec  14004  prdsbas3  14440  prdsdsval2  14443  invfuc  14905  yonedalem4c  15108  gsumconst  16449  prdsgsum  16493  prdsgsumOLD  16494  dprdwd  16517  dprdwdOLD  16523  gsumdixpOLD  16722  gsumdixp  16723  evlslem4OLD  17612  evlslem4  17613  elptr2  19169  ptunimpt  19190  ptcldmpt  19209  ptclsg  19210  txcnp  19215  ptcnplem  19216  cnmpt11  19258  cnmpt1t  19260  cnmptk2  19281  xkocnv  19409  flfcnp2  19602  ustn0  19817  utopsnneiplem  19844  ucnima  19878  iccpnfcnv  20538  ovolctb  20995  ovoliunlem1  21007  ovoliun2  21011  ovolshftlem1  21014  ovolscalem1  21018  voliun  21057  ioombl1lem3  21063  ioombl1lem4  21064  uniioombllem2  21085  mbfeqalem  21142  mbfpos  21151  mbfposr  21152  mbfposb  21153  mbfsup  21164  mbfinf  21165  mbflim  21168  i1fposd  21207  itg1climres  21214  mbfi1fseqlem4  21218  mbfi1fseqlem5  21219  mbfi1fseqlem6  21220  itg2split  21249  itg2mono  21253  itg2cnlem1  21261  isibl2  21266  itgmpt  21282  itgeqa  21313  itggt0  21341  itgcn  21342  limcmpt  21380  dvlipcn  21488  lhop2  21509  dvfsumabs  21517  itgparts  21541  itgsubstlem  21542  itgsubst  21543  elplyd  21692  coeeulem  21714  coeeq2  21732  dvply1  21772  plyremlem  21792  ulmss  21884  ulmdvlem1  21887  mtest  21891  itgulm2  21896  radcnvlem1  21900  pserulm  21909  leibpi  22359  rlimcnp  22381  o1cxp  22390  sqff1o  22542  lgseisenlem2  22711  dchrvmasumlem1  22766  ubthlem1  24293  cnlnadjlem5  25497  xppreima2  25987  abfmpunirn  25989  fpwrelmap  26055  xrmulc1cn  26382  esumpcvgval  26549  voliune  26667  eulerpartgbij  26777  signsplypnf  26973  lgamgulmlem2  27038  lgamgulmlem6  27042  lgamgulm2  27044  iscvm  27170  prodrblem  27464  fprodcvg  27465  prodmolem2a  27469  zprod  27472  fprod  27476  fprodmul  27493  fproddiv  27494  itg2addnclem  28469  itggt0cn  28490  ftc1anclem5  28497  elrfirn2  29058  eq0rabdioph  29141  monotoddzz  29310  aomclem2  29434  refsumcn  29778  refsum2cnlem1  29785  fmuldfeqlem1  29789  fmuldfeq  29790  climneg  29809  climdivf  29811  itgsin0pilem1  29816  ibliccsinexp  29817  itgsinexplem1  29820  itgsinexp  29821  stoweidlem2  29823  stoweidlem11  29832  stoweidlem12  29833  stoweidlem16  29837  stoweidlem17  29838  stoweidlem18  29839  stoweidlem19  29840  stoweidlem20  29841  stoweidlem21  29842  stoweidlem22  29843  stoweidlem23  29844  stoweidlem27  29848  stoweidlem31  29852  stoweidlem34  29855  stoweidlem36  29857  stoweidlem40  29861  stoweidlem41  29862  stoweidlem42  29863  stoweidlem48  29869  stoweidlem55  29876  stoweidlem59  29880  stoweidlem62  29883  stirlinglem3  29897  stirlinglem8  29902  stirlinglem14  29908  stirlinglem15  29909  stirlingr  29911  frgrancvvdeqlem6  30654