Theorem fvmpt2 6945

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

Hypothesis

Ref	Expression
mptrcl.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fvmpt2	⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt2

Step	Hyp	Ref	Expression
1		mptrcl.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	fvmpt2i 6944	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵))
3		fvi 6903	. 2 ⊢ (𝐵 ∈ 𝐶 → ( I ‘𝐵) = 𝐵)
4	2, 3	sylan9eq 2784	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176   I cid 5517  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmptss  6946  fvmpt2d  6947  fvmptd3f  6949  mpteqb  6953  fvmptt  6954  fvmptf  6955  fnmptfvd  6979  ralrnmptw  7032  ralrnmpt  7034  fompt  7056  fmptco  7067  f1mpt  7202  offval2  7637  ofrfval2  7638  fimaproj  8075  mptelixpg  8869  dom2lem  8924  mapxpen  9067  xpmapenlem  9068  cnfcom3clem  9620  tcvalg  9653  rankf  9709  infxpenc2lem2  9933  dfac8clem  9945  acni2  9959  acnlem  9961  fin23lem32  10257  axcc2lem  10349  axcc3  10351  domtriomlem  10355  ac6num  10392  konigthlem  10481  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  seqof  13984  seqof2  13985  rlim2  15421  ello1mpt  15446  o1compt  15512  sumrblem  15636  fsumcvg  15637  summolem2a  15640  fsum  15645  fsumcvg2  15652  fsumadd  15665  isummulc2  15687  fsummulc2  15709  fsumrelem  15732  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  zprod  15862  fprod  15866  fprodmul  15885  fproddiv  15886  iserodd  16765  prmrec  16852  prdsbas3  17403  prdsdsval2  17406  invfuc  17902  yonedalem4c  18201  smndex1n0mnd  18804  gsumconst  19831  prdsgsum  19878  gsumdixp  20222  evlslem4  21999  elptr2  23477  ptunimpt  23498  ptcldmpt  23517  ptclsg  23518  txcnp  23523  ptcnplem  23524  cnmpt11  23566  cnmpt1t  23568  cnmptk2  23589  xkocnv  23717  flfcnp2  23910  ustn0  24124  utopsnneiplem  24151  ucnima  24184  iccpnfcnv  24858  ovolctb  25407  ovoliunlem1  25419  ovoliun2  25423  ovolshftlem1  25426  ovolscalem1  25430  voliun  25471  ioombl1lem3  25477  ioombl1lem4  25478  uniioombllem2  25500  mbfeqalem1  25558  mbfpos  25568  mbfposr  25569  mbfposb  25570  mbfsup  25581  mbfinf  25582  mbflim  25585  i1fposd  25624  itg1climres  25631  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  itg2split  25666  itg2mono  25670  itg2cnlem1  25678  isibl2  25683  itgmpt  25700  itgeqa  25731  itggt0  25761  itgcn  25762  limcmpt  25800  dvlipcn  25915  lhop2  25936  dvfsumabs  25945  itgparts  25970  itgsubstlem  25971  itgsubst  25972  elplyd  26123  coeeulem  26145  coeeq2  26163  dvply1  26207  plyremlem  26228  ulmss  26322  ulmdvlem1  26325  mtest  26329  itgulm2  26334  radcnvlem1  26338  pserulm  26347  leibpi  26868  rlimcnp  26891  o1cxp  26901  lgamgulmlem2  26956  lgamgulmlem6  26960  lgamgulm2  26962  sqff1o  27108  lgseisenlem2  27303  dchrvmasumlem1  27422  frgrncvvdeqlem5  30265  ubthlem1  30832  cnlnadjlem5  32033  xppreima2  32608  abfmpunirn  32609  aciunf1lem  32619  suppovss  32637  fpwrelmap  32689  nsgmgc  33359  zringfrac  33501  algextdeglem6  33688  xrmulc1cn  33896  esumpcvgval  34044  esumsup  34055  voliune  34195  eulerpartgbij  34339  signsplypnf  34517  wevgblacfn  35081  iscvm  35231  mclsrcl  35533  f1omptsnlem  37309  matunitlindflem2  37596  itg2addnclem  37650  itggt0cn  37669  ftc1anclem5  37676  pwsgprod  42517  elrfirn2  42669  eq0rabdioph  42749  monotoddzz  42916  aomclem2  43028  refsumcn  45008  refsum2cnlem1  45015  fvmpt2bd  45148  choicefi  45178  axccdom  45200  fvmpt4  45216  fsumsermpt  45561  fmuldfeqlem1  45564  fmuldfeq  45565  climneg  45592  climdivf  45594  mullimc  45598  idlimc  45608  sumnnodd  45612  neglimc  45629  addlimc  45630  0ellimcdiv  45631  climfveqmpt2  45675  climeqmpt  45679  limsupequzmptlem  45710  liminfvalxr  45765  xlimmnfmpt  45825  xlimpnfmpt  45826  cncfmptssg  45853  cncfshift  45856  icccncfext  45869  cncfiooicclem1  45875  fprodsubrecnncnvlem  45889  fprodaddrecnncnvlem  45891  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnmptdivc  45920  dvnmul  45925  dvnprodlem2  45929  itgsin0pilem1  45932  ibliccsinexp  45933  itgsinexplem1  45936  itgsinexp  45937  ditgeqiooicc  45942  itgsubsticclem  45957  itgioocnicc  45959  stoweidlem2  45984  stoweidlem11  45993  stoweidlem12  45994  stoweidlem16  45998  stoweidlem17  45999  stoweidlem18  46000  stoweidlem19  46001  stoweidlem20  46002  stoweidlem21  46003  stoweidlem22  46004  stoweidlem23  46005  stoweidlem27  46009  stoweidlem31  46013  stoweidlem34  46016  stoweidlem36  46018  stoweidlem40  46022  stoweidlem41  46023  stoweidlem42  46024  stoweidlem48  46030  stoweidlem55  46037  stoweidlem59  46041  stoweidlem62  46044  stirlinglem3  46058  stirlinglem8  46063  stirlinglem14  46069  stirlinglem15  46070  stirlingr  46072  dirkeritg  46084  dirkercncflem2  46086  fourierdlem14  46103  fourierdlem31  46120  fourierdlem41  46130  fourierdlem48  46136  fourierdlem49  46137  fourierdlem50  46138  fourierdlem51  46139  fourierdlem56  46144  fourierdlem60  46148  fourierdlem61  46149  fourierdlem66  46154  fourierdlem70  46158  fourierdlem71  46159  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem77  46165  fourierdlem78  46166  fourierdlem81  46169  fourierdlem83  46171  fourierdlem84  46172  fourierdlem85  46173  fourierdlem87  46175  fourierdlem88  46176  fourierdlem89  46177  fourierdlem91  46179  fourierdlem92  46180  fourierdlem93  46181  fourierdlem95  46183  fourierdlem97  46185  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fourierdlem112  46200  sqwvfoura  46210  sqwvfourb  46211  fouriersw  46213  elaa2lem  46215  etransclem4  46220  etransclem13  46229  etransclem35  46251  etransclem46  46262  etransclem48  46264  sge0revalmpt  46360  sge0fsummpt  46372  sge0iunmptlemfi  46395  sge0iunmptlemre  46397  sge0ltfirpmpt2  46408  sge0fsummptf  46418  nnfoctbdjlem  46437  iundjiun  46442  meaiunlelem  46450  meaiuninclem  46462  meaiuninc3v  46466  omeiunlempt  46502  carageniuncllem2  46504  caratheodorylem2  46509  0ome  46511  isomenndlem  46512  hoicvr  46530  hoicvrrex  46538  ovn0lem  46547  ovnsubaddlem1  46552  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoilem2  46584  hoicoto2  46587  hoi2toco  46589  ovnlecvr2  46592  ovncvr2  46593  ovnsubadd2lem  46627  ovolval5lem2  46635  ovnovollem1  46638  ovnovollem2  46639  vonioolem1  46662  smfaddlem1  46745  smflimlem2  46754  smflimmpt  46792  smflimsuplem2  46803  smflimsuplem4  46805  smflimsuplem5  46806  smflimsupmpt  46811  smfliminfmpt  46814  smfsupdmmbllem  46826  finfdm  46828  smfinfdmmbllem  46830  setrec2mpt  49683  aacllem  49787