Theorem fvmpt2 6895

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 6894	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵))
3		fvi 6853	. 2 ⊢ (𝐵 ∈ 𝐶 → ( I ‘𝐵) = 𝐵)
4	2, 3	sylan9eq 2799	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ↦ cmpt 5158   I cid 5489  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fvmptss  6896  fvmpt2d  6897  fvmptd3f  6899  mpteqb  6903  fvmptt  6904  fvmptf  6905  fnmptfvd  6927  ralrnmptw  6979  ralrnmpt  6981  fmptco  7010  f1mpt  7143  offval2  7562  ofrfval2  7563  fimaproj  7985  mptelixpg  8732  dom2lem  8789  mapxpen  8939  xpmapenlem  8940  cnfcom3clem  9472  tcvalg  9505  rankf  9561  infxpenc2lem2  9785  dfac8clem  9797  acni2  9811  acnlem  9813  fin23lem32  10109  axcc2lem  10201  axcc3  10203  domtriomlem  10207  ac6num  10244  konigthlem  10333  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  seqof  13789  seqof2  13790  rlim2  15214  ello1mpt  15239  o1compt  15305  sumrblem  15432  fsumcvg  15433  summolem2a  15436  fsum  15441  fsumcvg2  15448  fsumadd  15461  isummulc2  15483  fsummulc2  15505  fsumrelem  15528  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  zprod  15656  fprod  15660  fprodmul  15679  fproddiv  15680  iserodd  16545  prmrec  16632  prdsbas3  17201  prdsdsval2  17204  invfuc  17701  yonedalem4c  18004  smndex1n0mnd  18560  gsumconst  19544  prdsgsum  19591  gsumdixp  19857  evlslem4  21293  elptr2  22734  ptunimpt  22755  ptcldmpt  22774  ptclsg  22775  txcnp  22780  ptcnplem  22781  cnmpt11  22823  cnmpt1t  22825  cnmptk2  22846  xkocnv  22974  flfcnp2  23167  ustn0  23381  utopsnneiplem  23408  ucnima  23442  iccpnfcnv  24116  ovolctb  24663  ovoliunlem1  24675  ovoliun2  24679  ovolshftlem1  24682  ovolscalem1  24686  voliun  24727  ioombl1lem3  24733  ioombl1lem4  24734  uniioombllem2  24756  mbfeqalem1  24814  mbfpos  24824  mbfposr  24825  mbfposb  24826  mbfsup  24837  mbfinf  24838  mbflim  24841  i1fposd  24881  itg1climres  24888  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2split  24923  itg2mono  24927  itg2cnlem1  24935  isibl2  24940  itgmpt  24956  itgeqa  24987  itggt0  25017  itgcn  25018  limcmpt  25056  dvlipcn  25167  lhop2  25188  dvfsumabs  25196  itgparts  25220  itgsubstlem  25221  itgsubst  25222  elplyd  25372  coeeulem  25394  coeeq2  25412  dvply1  25453  plyremlem  25473  ulmss  25565  ulmdvlem1  25568  mtest  25572  itgulm2  25577  radcnvlem1  25581  pserulm  25590  leibpi  26101  rlimcnp  26124  o1cxp  26133  lgamgulmlem2  26188  lgamgulmlem6  26192  lgamgulm2  26194  sqff1o  26340  lgseisenlem2  26533  dchrvmasumlem1  26652  frgrncvvdeqlem5  28676  ubthlem1  29241  cnlnadjlem5  30442  xppreima2  30997  abfmpunirn  30998  aciunf1lem  31008  suppovss  31026  fpwrelmap  31077  nsgmgc  31606  xrmulc1cn  31889  esumpcvgval  32055  esumsup  32066  voliune  32206  eulerpartgbij  32348  signsplypnf  32538  iscvm  33230  mclsrcl  33532  f1omptsnlem  35516  matunitlindflem2  35783  itg2addnclem  35837  itggt0cn  35856  ftc1anclem5  35863  pwsgprod  40276  elrfirn2  40525  eq0rabdioph  40605  monotoddzz  40772  aomclem2  40887  refsumcn  42580  refsum2cnlem1  42587  fvmpt2bd  42713  fompt  42737  choicefi  42747  axccdom  42769  fvmpt4  42789  fsumsermpt  43127  fmuldfeqlem1  43130  fmuldfeq  43131  climneg  43158  climdivf  43160  mullimc  43164  idlimc  43174  sumnnodd  43178  neglimc  43195  addlimc  43196  0ellimcdiv  43197  climfveqmpt2  43241  climeqmpt  43245  limsupequzmptlem  43276  liminfvalxr  43331  xlimmnfmpt  43391  xlimpnfmpt  43392  cncfmptssg  43419  cncfshift  43422  icccncfext  43435  cncfiooicclem1  43441  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmptdivc  43486  dvnmul  43491  dvnprodlem2  43495  itgsin0pilem1  43498  ibliccsinexp  43499  itgsinexplem1  43502  itgsinexp  43503  ditgeqiooicc  43508  itgsubsticclem  43523  itgioocnicc  43525  stoweidlem2  43550  stoweidlem11  43559  stoweidlem12  43560  stoweidlem16  43564  stoweidlem17  43565  stoweidlem18  43566  stoweidlem19  43567  stoweidlem20  43568  stoweidlem21  43569  stoweidlem22  43570  stoweidlem23  43571  stoweidlem27  43575  stoweidlem31  43579  stoweidlem34  43582  stoweidlem36  43584  stoweidlem40  43588  stoweidlem41  43589  stoweidlem42  43590  stoweidlem48  43596  stoweidlem55  43603  stoweidlem59  43607  stoweidlem62  43610  stirlinglem3  43624  stirlinglem8  43629  stirlinglem14  43635  stirlinglem15  43636  stirlingr  43638  dirkeritg  43650  dirkercncflem2  43652  fourierdlem14  43669  fourierdlem31  43686  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem56  43710  fourierdlem60  43714  fourierdlem61  43715  fourierdlem66  43720  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem77  43731  fourierdlem78  43732  fourierdlem81  43735  fourierdlem83  43737  fourierdlem84  43738  fourierdlem85  43739  fourierdlem87  43741  fourierdlem88  43742  fourierdlem89  43743  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem95  43749  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  elaa2lem  43781  etransclem4  43786  etransclem13  43795  etransclem35  43817  etransclem46  43828  etransclem48  43830  sge0revalmpt  43923  sge0fsummpt  43935  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0ltfirpmpt2  43971  sge0fsummptf  43981  nnfoctbdjlem  44000  iundjiun  44005  meaiunlelem  44013  meaiuninclem  44025  meaiuninc3v  44029  omeiunlempt  44065  carageniuncllem2  44067  caratheodorylem2  44072  0ome  44074  isomenndlem  44075  hoicvr  44093  hoicvrrex  44101  ovn0lem  44110  ovnsubaddlem1  44115  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem2  44147  hoicoto2  44150  hoi2toco  44152  ovnlecvr2  44155  ovncvr2  44156  ovnsubadd2lem  44190  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  vonioolem1  44225  smfaddlem1  44308  smflimlem2  44317  smflimmpt  44354  smfinfmpt  44363  smflimsuplem2  44365  smflimsuplem4  44367  smflimsuplem5  44368  smflimsupmpt  44373  smfliminfmpt  44376  aacllem  46516