Theorem fvmpt2 6291

Description: Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)

Hypothesis

Ref	Expression
mptrcl.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		mptrcl.1	. . 3 |- F = ( x e. A |-> B )
2	1	fvmpt2i 6290	. 2 |- ( x e. A -> ( F ` x ) = ( _I ` B ) )
3		fvi 6255	. 2 |- ( B e. C -> ( _I ` B ) = B )
4	2, 3	sylan9eq 2676	1 |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   |-> cmpt 4729   _I cid 5023   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  fvmptss  6292  fvmpt2d  6293  fvmptd3f  6295  mpteqb  6299  fvmptt  6300  fvmptf  6301  fnmptfvd  6320  ralrnmpt  6368  fmptco  6396  f1mpt  6518  offval2  6914  ofrfval2  6915  mptelixpg  7945  dom2lem  7995  mapxpen  8126  xpmapenlem  8127  cnfcom3clem  8602  tcvalg  8614  rankf  8657  infxpenc2lem2  8843  dfac8clem  8855  acni2  8869  acnlem  8871  fin23lem32  9166  axcc2lem  9258  axcc3  9260  domtriomlem  9264  ac6num  9301  konigthlem  9390  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  seqof  12858  seqof2  12859  rlim2  14227  ello1mpt  14252  o1compt  14318  sumrblem  14442  fsumcvg  14443  summolem2a  14446  fsum  14451  fsumcvg2  14458  fsumadd  14470  isummulc2  14493  fsummulc2  14516  fsumrelem  14539  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  fprod  14671  fprodmul  14690  fproddiv  14691  iserodd  15540  prmrec  15626  prdsbas3  16141  prdsdsval2  16144  invfuc  16634  yonedalem4c  16917  gsumconst  18334  prdsgsum  18377  gsumdixp  18609  evlslem4  19508  elptr2  21377  ptunimpt  21398  ptcldmpt  21417  ptclsg  21418  txcnp  21423  ptcnplem  21424  cnmpt11  21466  cnmpt1t  21468  cnmptk2  21489  xkocnv  21617  flfcnp2  21811  ustn0  22024  utopsnneiplem  22051  ucnima  22085  iccpnfcnv  22743  ovolctb  23258  ovoliunlem1  23270  ovoliun2  23274  ovolshftlem1  23277  ovolscalem1  23281  voliun  23322  ioombl1lem3  23328  ioombl1lem4  23329  uniioombllem2  23351  mbfeqalem  23409  mbfpos  23418  mbfposr  23419  mbfposb  23420  mbfsup  23431  mbfinf  23432  mbflim  23435  i1fposd  23474  itg1climres  23481  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2split  23516  itg2mono  23520  itg2cnlem1  23528  isibl2  23533  itgmpt  23549  itgeqa  23580  itggt0  23608  itgcn  23609  limcmpt  23647  dvlipcn  23757  lhop2  23778  dvfsumabs  23786  itgparts  23810  itgsubstlem  23811  itgsubst  23812  elplyd  23958  coeeulem  23980  coeeq2  23998  dvply1  24039  plyremlem  24059  ulmss  24151  ulmdvlem1  24154  mtest  24158  itgulm2  24163  radcnvlem1  24167  pserulm  24176  leibpi  24669  rlimcnp  24692  o1cxp  24701  lgamgulmlem2  24756  lgamgulmlem6  24760  lgamgulm2  24762  sqff1o  24908  lgseisenlem2  25101  dchrvmasumlem1  25184  frgrncvvdeqlem5  27167  ubthlem1  27726  cnlnadjlem5  28930  xppreima2  29450  abfmpunirn  29452  aciunf1lem  29462  fpwrelmap  29508  fimaproj  29900  xrmulc1cn  29976  esumpcvgval  30140  esumsup  30151  voliune  30292  eulerpartgbij  30434  signsplypnf  30627  iscvm  31241  mclsrcl  31458  f1omptsnlem  33183  matunitlindflem2  33406  itg2addnclem  33461  itggt0cn  33482  ftc1anclem5  33489  elrfirn2  37259  eq0rabdioph  37340  monotoddzz  37508  aomclem2  37625  refsumcn  39189  refsum2cnlem1  39196  fvmpt2bd  39350  wessf1ornlem  39371  fompt  39379  projf1o  39386  choicefi  39392  axccdom  39416  fvmpt4  39446  fsumsermpt  39811  fmuldfeqlem1  39814  fmuldfeq  39815  climneg  39842  climdivf  39844  mullimc  39848  idlimc  39858  sumnnodd  39862  neglimc  39879  addlimc  39880  0ellimcdiv  39881  climfveqmpt2  39925  climeqmpt  39929  limsupequzmptlem  39960  liminfvalxr  40015  xlimmnfmpt  40069  xlimpnfmpt  40070  cncfmptssg  40083  cncfshift  40087  icccncfext  40100  cncfiooicclem1  40106  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmptdivc  40153  dvnmul  40158  dvnprodlem2  40162  itgsin0pilem1  40165  ibliccsinexp  40166  itgsinexplem1  40169  itgsinexp  40170  ditgeqiooicc  40176  itgsubsticclem  40191  itgioocnicc  40193  stoweidlem2  40219  stoweidlem11  40228  stoweidlem12  40229  stoweidlem16  40233  stoweidlem17  40234  stoweidlem18  40235  stoweidlem19  40236  stoweidlem20  40237  stoweidlem21  40238  stoweidlem22  40239  stoweidlem23  40240  stoweidlem27  40244  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem40  40257  stoweidlem41  40258  stoweidlem42  40259  stoweidlem48  40265  stoweidlem55  40272  stoweidlem59  40276  stoweidlem62  40279  stirlinglem3  40293  stirlinglem8  40298  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirkeritg  40319  dirkercncflem2  40321  fourierdlem14  40338  fourierdlem31  40355  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem56  40379  fourierdlem60  40383  fourierdlem61  40384  fourierdlem66  40389  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem77  40400  fourierdlem78  40401  fourierdlem81  40404  fourierdlem83  40406  fourierdlem84  40407  fourierdlem85  40408  fourierdlem87  40410  fourierdlem88  40411  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  elaa2lem  40450  etransclem4  40455  etransclem13  40464  etransclem35  40486  etransclem46  40497  etransclem48  40499  sge0revalmpt  40595  sge0fsummpt  40607  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0ltfirpmpt2  40643  sge0fsummptf  40653  nnfoctbdjlem  40672  iundjiun  40677  meaiunlelem  40685  meaiuninclem  40697  omeiunlempt  40734  carageniuncllem2  40736  caratheodorylem2  40741  0ome  40743  isomenndlem  40744  hoicvr  40762  hoicvrrex  40770  ovn0lem  40779  ovnsubaddlem1  40784  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem2  40816  hoicoto2  40819  hoi2toco  40821  ovnlecvr2  40824  ovncvr2  40825  ovnsubadd2lem  40859  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  vonioolem1  40894  smfaddlem1  40971  smflimlem2  40980  smflimmpt  41016  smfsupmpt  41021  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem4  41029  smflimsuplem5  41030  smflimsupmpt  41035  smfliminfmpt  41038  aacllem  42547