Theorem fvmpt2 5957

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

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   e. wcel 1887   |-> cmpt 4461   _I cid 4744   ` cfv 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fv 5590

This theorem is referenced by:  fvmptss  5958  fvmpt2d  5959  fvmptdf  5961  mpteqb  5964  fvmptt  5965  fvmptf  5966  fnmptfvd  5985  ralrnmpt  6031  fmptco  6056  f1mpt  6162  offval2  6548  ofrfval2  6549  mptelixpg  7559  dom2lem  7609  mapxpen  7738  xpmapenlem  7739  cnfcom3clem  8210  tcvalg  8222  rankf  8265  infxpenc2lem2  8451  dfac8clem  8463  acni2  8477  acnlem  8479  fin23lem32  8774  axcc2lem  8866  axcc3  8868  domtriomlem  8872  ac6num  8909  konigthlem  8993  rpnnen1lem1  11290  rpnnen1lem3  11292  rpnnen1lem5  11294  seqof  12270  seqof2  12271  rlim2  13560  ello1mpt  13585  o1compt  13651  sumrblem  13777  fsumcvg  13778  summolem2a  13781  fsum  13786  fsumcvg2  13793  fsumadd  13805  isummulc2  13823  fsummulc2  13845  fsumrelem  13867  prodrblem  13983  fprodcvg  13984  prodmolem2a  13988  zprod  13991  fprod  13995  fprodmul  14014  fproddiv  14015  iserodd  14785  prmrec  14866  prdsbas3  15379  prdsdsval2  15382  invfuc  15879  yonedalem4c  16162  gsumconst  17567  prdsgsum  17610  dprdwdOLD  17644  gsumdixp  17837  evlslem4  18731  elptr2  20589  ptunimpt  20610  ptcldmpt  20629  ptclsg  20630  txcnp  20635  ptcnplem  20636  cnmpt11  20678  cnmpt1t  20680  cnmptk2  20701  xkocnv  20829  flfcnp2  21022  ustn0  21235  utopsnneiplem  21262  ucnima  21296  iccpnfcnv  21972  ovolctb  22443  ovoliunlem1  22455  ovoliun2  22459  ovolshftlem1  22462  ovolscalem1  22466  voliun  22507  ioombl1lem3  22513  ioombl1lem4  22514  uniioombllem2  22540  uniioombllem2OLD  22541  mbfeqalem  22598  mbfpos  22607  mbfposr  22608  mbfposb  22609  mbfsup  22620  mbfinf  22621  mbfinfOLD  22622  mbflim  22626  i1fposd  22665  itg1climres  22672  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  itg2split  22707  itg2mono  22711  itg2cnlem1  22719  isibl2  22724  itgmpt  22740  itgeqa  22771  itggt0  22799  itgcn  22800  limcmpt  22838  dvlipcn  22946  lhop2  22967  dvfsumabs  22975  itgparts  22999  itgsubstlem  23000  itgsubst  23001  elplyd  23156  coeeulem  23178  coeeq2  23196  dvply1  23237  plyremlem  23257  ulmss  23352  ulmdvlem1  23355  mtest  23359  itgulm2  23364  radcnvlem1  23368  pserulm  23377  leibpi  23868  rlimcnp  23891  o1cxp  23900  lgamgulmlem2  23955  lgamgulmlem6  23959  lgamgulm2  23961  sqff1o  24109  lgseisenlem2  24278  dchrvmasumlem1  24333  frgrancvvdeqlem6  25763  ubthlem1  26512  cnlnadjlem5  27724  xppreima2  28249  abfmpunirn  28251  aciunf1lem  28264  fpwrelmap  28318  fimaproj  28660  xrmulc1cn  28736  esumpcvgval  28899  esumsup  28910  voliune  29052  eulerpartgbij  29205  signsplypnf  29439  iscvm  29982  mclsrcl  30199  f1omptsnlem  31738  itg2addnclem  31993  itggt0cn  32014  ftc1anclem5  32021  elrfirn2  35538  eq0rabdioph  35619  monotoddzz  35791  aomclem2  35913  refsumcn  37351  refsum2cnlem1  37358  fvmpt2bd  37434  wessf1ornlem  37459  fompt  37467  projf1o  37474  choicefi  37481  fmuldfeqlem1  37660  fmuldfeq  37661  climneg  37689  climdivf  37692  mullimc  37696  idlimc  37706  sumnnodd  37710  neglimc  37728  addlimc  37729  0ellimcdiv  37730  cncfmptssg  37747  cncfshift  37751  icccncfext  37765  cncfiooicclem1  37771  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnmptdivc  37813  dvnmul  37818  dvnprodlem2  37822  itgsin0pilem1  37826  ibliccsinexp  37827  itgsinexplem1  37830  itgsinexp  37831  ditgeqiooicc  37837  itgsubsticclem  37852  itgioocnicc  37854  stoweidlem2  37862  stoweidlem11  37871  stoweidlem12  37872  stoweidlem16  37876  stoweidlem17  37877  stoweidlem18  37878  stoweidlem19  37879  stoweidlem20  37880  stoweidlem21  37881  stoweidlem22  37882  stoweidlem23  37883  stoweidlem27  37887  stoweidlem31  37892  stoweidlem34  37895  stoweidlem36  37897  stoweidlem40  37901  stoweidlem41  37902  stoweidlem42  37903  stoweidlem48  37909  stoweidlem55  37916  stoweidlem59  37920  stoweidlem62  37923  stoweidlem62OLD  37924  stirlinglem3  37938  stirlinglem8  37943  stirlinglem14  37949  stirlinglem15  37950  stirlingr  37952  dirkeritg  37964  dirkercncflem2  37966  fourierdlem14  37983  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem41  38011  fourierdlem48  38018  fourierdlem49  38019  fourierdlem50  38020  fourierdlem51  38021  fourierdlem56  38026  fourierdlem60  38030  fourierdlem61  38031  fourierdlem66  38036  fourierdlem70  38040  fourierdlem71  38041  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem77  38047  fourierdlem78  38048  fourierdlem81  38051  fourierdlem83  38053  fourierdlem84  38054  fourierdlem85  38055  fourierdlem87  38057  fourierdlem88  38058  fourierdlem89  38059  fourierdlem91  38061  fourierdlem92  38062  fourierdlem93  38063  fourierdlem95  38065  fourierdlem97  38067  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  fourierdlem112  38082  sqwvfoura  38092  sqwvfourb  38093  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem4  38103  etransclem13  38112  etransclem35  38134  etransclem46  38145  etransclem48OLD  38147  etransclem48  38148  sge0revalmpt  38220  sge0fsummpt  38232  sge0iunmptlemfi  38255  sge0iunmptlemre  38257  sge0ltfirpmpt2  38268  sge0fsummptf  38278  nnfoctbdjlem  38293  iundjiun  38298  meaiunlelem  38306  omeiunlempt  38341  carageniuncllem2  38343  caratheodorylem2  38348  0ome  38350  isomenndlem  38351  hoicvr  38370  hoicvrrex  38378  ovn0lem  38387  ovnsubaddlem1  38392  hoidmvlelem2  38418  hoidmvlelem3  38419  ovnhoilem2  38424  hoicoto2  38427  hoi2toco  38429  ovnlecvr2  38432  ovncvr2  38433  aacllem  40593