Theorem fvmpt2 5939

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

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   e. wcel 1823   |-> cmpt 4497   _I cid 4779   ` cfv 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fv 5578

This theorem is referenced by:  fvmptss  5940  fvmpt2d  5941  fvmptdf  5943  mpteqb  5946  fvmptt  5947  fvmptf  5948  fnmptfvd  5966  ralrnmpt  6016  fmptco  6040  f1mpt  6144  offval2  6529  ofrfval2  6530  mptelixpg  7499  dom2lem  7548  mapxpen  7676  xpmapenlem  7677  cnfcom3clem  8140  cnfcom3clemOLD  8148  tcvalg  8160  rankf  8203  infxpenc2lem2  8388  infxpenc2lem2OLD  8392  dfac8clem  8404  acni2  8418  acnlem  8420  fin23lem32  8715  axcc2lem  8807  axcc3  8809  domtriomlem  8813  ac6num  8850  konigthlem  8934  rpnnen1lem1  11209  rpnnen1lem3  11211  rpnnen1lem5  11213  seqof  12146  seqof2  12147  rlim2  13401  ello1mpt  13426  o1compt  13492  sumrblem  13615  fsumcvg  13616  summolem2a  13619  fsum  13624  fsumcvg2  13631  fsumadd  13643  isummulc2  13659  fsummulc2  13681  fsumrelem  13703  prodrblem  13818  fprodcvg  13819  prodmolem2a  13823  zprod  13826  fprod  13830  fprodmul  13847  fproddiv  13848  iserodd  14443  prmrec  14524  prdsbas3  14970  prdsdsval2  14973  invfuc  15462  yonedalem4c  15745  gsumconst  17152  prdsgsum  17202  prdsgsumOLD  17203  dprdwdOLD2  17240  dprdwdOLD  17246  gsumdixpOLD  17452  gsumdixp  17453  evlslem4OLD  18368  evlslem4  18369  elptr2  20241  ptunimpt  20262  ptcldmpt  20281  ptclsg  20282  txcnp  20287  ptcnplem  20288  cnmpt11  20330  cnmpt1t  20332  cnmptk2  20353  xkocnv  20481  flfcnp2  20674  ustn0  20889  utopsnneiplem  20916  ucnima  20950  iccpnfcnv  21610  ovolctb  22067  ovoliunlem1  22079  ovoliun2  22083  ovolshftlem1  22086  ovolscalem1  22090  voliun  22130  ioombl1lem3  22136  ioombl1lem4  22137  uniioombllem2  22158  mbfeqalem  22215  mbfpos  22224  mbfposr  22225  mbfposb  22226  mbfsup  22237  mbfinf  22238  mbflim  22241  i1fposd  22280  itg1climres  22287  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  mbfi1fseqlem6  22293  itg2split  22322  itg2mono  22326  itg2cnlem1  22334  isibl2  22339  itgmpt  22355  itgeqa  22386  itggt0  22414  itgcn  22415  limcmpt  22453  dvlipcn  22561  lhop2  22582  dvfsumabs  22590  itgparts  22614  itgsubstlem  22615  itgsubst  22616  elplyd  22765  coeeulem  22787  coeeq2  22805  dvply1  22846  plyremlem  22866  ulmss  22958  ulmdvlem1  22961  mtest  22965  itgulm2  22970  radcnvlem1  22974  pserulm  22983  leibpi  23470  rlimcnp  23493  o1cxp  23502  sqff1o  23654  lgseisenlem2  23823  dchrvmasumlem1  23878  frgrancvvdeqlem6  25237  ubthlem1  25984  cnlnadjlem5  27188  xppreima2  27709  abfmpunirn  27711  aciunf1lem  27729  fpwrelmap  27787  fimaproj  28071  xrmulc1cn  28147  esumpcvgval  28307  esumsup  28318  voliune  28438  eulerpartgbij  28575  signsplypnf  28771  lgamgulmlem2  28836  lgamgulmlem6  28840  lgamgulm2  28842  iscvm  28968  mclsrcl  29185  itg2addnclem  30306  itggt0cn  30327  ftc1anclem5  30334  elrfirn2  30868  eq0rabdioph  30949  monotoddzz  31118  aomclem2  31240  refsumcn  31645  refsum2cnlem1  31652  fvmpt2bd  31686  fmuldfeqlem1  31815  fmuldfeq  31816  climneg  31855  climdivf  31857  mullimc  31861  idlimc  31871  sumnnodd  31875  neglimc  31892  addlimc  31893  0ellimcdiv  31894  cncfmptssg  31911  cncfshift  31915  icccncfext  31929  cncfiooicclem1  31935  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnmptdivc  31974  dvnmul  31979  dvnprodlem2  31983  itgsin0pilem1  31987  ibliccsinexp  31988  itgsinexplem1  31991  itgsinexp  31992  ditgeqiooicc  31998  itgsubsticclem  32013  itgioocnicc  32015  stoweidlem2  32023  stoweidlem11  32032  stoweidlem12  32033  stoweidlem16  32037  stoweidlem17  32038  stoweidlem18  32039  stoweidlem19  32040  stoweidlem20  32041  stoweidlem21  32042  stoweidlem22  32043  stoweidlem23  32044  stoweidlem27  32048  stoweidlem31  32052  stoweidlem34  32055  stoweidlem36  32057  stoweidlem40  32061  stoweidlem41  32062  stoweidlem42  32063  stoweidlem48  32069  stoweidlem55  32076  stoweidlem59  32080  stoweidlem62  32083  stirlinglem3  32097  stirlinglem8  32102  stirlinglem14  32108  stirlinglem15  32109  stirlingr  32111  dirkeritg  32123  dirkercncflem2  32125  fourierdlem14  32142  fourierdlem31  32159  fourierdlem41  32169  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem56  32184  fourierdlem60  32188  fourierdlem61  32189  fourierdlem66  32194  fourierdlem70  32198  fourierdlem71  32199  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem77  32205  fourierdlem78  32206  fourierdlem81  32209  fourierdlem83  32211  fourierdlem84  32212  fourierdlem85  32213  fourierdlem87  32215  fourierdlem88  32216  fourierdlem89  32217  fourierdlem91  32219  fourierdlem92  32220  fourierdlem93  32221  fourierdlem95  32223  fourierdlem97  32225  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fourierdlem112  32240  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  elaa2lem  32255  etransclem4  32260  etransclem13  32269  etransclem35  32291  etransclem46  32302  etransclem48  32304  aacllem  33604