Theorem fvmpt2 7015

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ↦ cmpt 5232   I cid 5575  ‘cfv 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fv 6557

This theorem is referenced by:  fvmptss  7016  fvmpt2d  7017  fvmptd3f  7019  mpteqb  7023  fvmptt  7024  fvmptf  7025  fnmptfvd  7049  ralrnmptw  7103  ralrnmpt  7105  fompt  7127  fmptco  7138  f1mpt  7271  offval2  7705  ofrfval2  7706  fimaproj  8140  mptelixpg  8954  dom2lem  9013  mapxpen  9171  xpmapenlem  9172  cnfcom3clem  9735  tcvalg  9768  rankf  9824  infxpenc2lem2  10050  dfac8clem  10062  acni2  10076  acnlem  10078  fin23lem32  10374  axcc2lem  10466  axcc3  10468  domtriomlem  10472  ac6num  10509  konigthlem  10598  rpnnen1lem1  13000  rpnnen1lem3  13001  rpnnen1lem5  13003  seqof  14065  seqof2  14066  rlim2  15481  ello1mpt  15506  o1compt  15572  sumrblem  15698  fsumcvg  15699  summolem2a  15702  fsum  15707  fsumcvg2  15714  fsumadd  15727  isummulc2  15749  fsummulc2  15771  fsumrelem  15794  prodrblem  15914  fprodcvg  15915  prodmolem2a  15919  zprod  15922  fprod  15926  fprodmul  15945  fproddiv  15946  iserodd  16812  prmrec  16899  prdsbas3  17471  prdsdsval2  17474  invfuc  17974  yonedalem4c  18277  smndex1n0mnd  18877  gsumconst  19906  prdsgsum  19953  gsumdixp  20272  evlslem4  22047  elptr2  23527  ptunimpt  23548  ptcldmpt  23567  ptclsg  23568  txcnp  23573  ptcnplem  23574  cnmpt11  23616  cnmpt1t  23618  cnmptk2  23639  xkocnv  23767  flfcnp2  23960  ustn0  24174  utopsnneiplem  24201  ucnima  24235  iccpnfcnv  24918  ovolctb  25468  ovoliunlem1  25480  ovoliun2  25484  ovolshftlem1  25487  ovolscalem1  25491  voliun  25532  ioombl1lem3  25538  ioombl1lem4  25539  uniioombllem2  25561  mbfeqalem1  25619  mbfpos  25629  mbfposr  25630  mbfposb  25631  mbfsup  25642  mbfinf  25643  mbflim  25646  i1fposd  25686  itg1climres  25693  mbfi1fseqlem4  25697  mbfi1fseqlem5  25698  mbfi1fseqlem6  25699  itg2split  25728  itg2mono  25732  itg2cnlem1  25740  isibl2  25745  itgmpt  25761  itgeqa  25792  itggt0  25822  itgcn  25823  limcmpt  25861  dvlipcn  25976  lhop2  25997  dvfsumabs  26006  itgparts  26031  itgsubstlem  26032  itgsubst  26033  elplyd  26186  coeeulem  26208  coeeq2  26226  dvply1  26268  plyremlem  26289  ulmss  26383  ulmdvlem1  26386  mtest  26390  itgulm2  26395  radcnvlem1  26399  pserulm  26408  leibpi  26924  rlimcnp  26947  o1cxp  26957  lgamgulmlem2  27012  lgamgulmlem6  27016  lgamgulm2  27018  sqff1o  27164  lgseisenlem2  27359  dchrvmasumlem1  27478  frgrncvvdeqlem5  30190  ubthlem1  30757  cnlnadjlem5  31958  xppreima2  32523  abfmpunirn  32524  aciunf1lem  32534  suppovss  32552  fpwrelmap  32602  nsgmgc  33229  zringfrac  33371  algextdeglem6  33523  xrmulc1cn  33664  esumpcvgval  33830  esumsup  33841  voliune  33981  eulerpartgbij  34125  signsplypnf  34315  iscvm  35002  mclsrcl  35304  f1omptsnlem  36948  matunitlindflem2  37223  itg2addnclem  37277  itggt0cn  37296  ftc1anclem5  37303  pwsgprod  41914  elrfirn2  42260  eq0rabdioph  42340  monotoddzz  42508  aomclem2  42623  refsumcn  44536  refsum2cnlem1  44543  fvmpt2bd  44684  choicefi  44714  axccdom  44736  fvmpt4  44753  fsumsermpt  45107  fmuldfeqlem1  45110  fmuldfeq  45111  climneg  45138  climdivf  45140  mullimc  45144  idlimc  45154  sumnnodd  45158  neglimc  45175  addlimc  45176  0ellimcdiv  45177  climfveqmpt2  45221  climeqmpt  45225  limsupequzmptlem  45256  liminfvalxr  45311  xlimmnfmpt  45371  xlimpnfmpt  45372  cncfmptssg  45399  cncfshift  45402  icccncfext  45415  cncfiooicclem1  45421  fprodsubrecnncnvlem  45435  fprodaddrecnncnvlem  45437  ioodvbdlimc1lem2  45460  ioodvbdlimc2lem  45462  dvnmptdivc  45466  dvnmul  45471  dvnprodlem2  45475  itgsin0pilem1  45478  ibliccsinexp  45479  itgsinexplem1  45482  itgsinexp  45483  ditgeqiooicc  45488  itgsubsticclem  45503  itgioocnicc  45505  stoweidlem2  45530  stoweidlem11  45539  stoweidlem12  45540  stoweidlem16  45544  stoweidlem17  45545  stoweidlem18  45546  stoweidlem19  45547  stoweidlem20  45548  stoweidlem21  45549  stoweidlem22  45550  stoweidlem23  45551  stoweidlem27  45555  stoweidlem31  45559  stoweidlem34  45562  stoweidlem36  45564  stoweidlem40  45568  stoweidlem41  45569  stoweidlem42  45570  stoweidlem48  45576  stoweidlem55  45583  stoweidlem59  45587  stoweidlem62  45590  stirlinglem3  45604  stirlinglem8  45609  stirlinglem14  45615  stirlinglem15  45616  stirlingr  45618  dirkeritg  45630  dirkercncflem2  45632  fourierdlem14  45649  fourierdlem31  45666  fourierdlem41  45676  fourierdlem48  45682  fourierdlem49  45683  fourierdlem50  45684  fourierdlem51  45685  fourierdlem56  45690  fourierdlem60  45694  fourierdlem61  45695  fourierdlem66  45700  fourierdlem70  45704  fourierdlem71  45705  fourierdlem73  45707  fourierdlem74  45708  fourierdlem75  45709  fourierdlem76  45710  fourierdlem77  45711  fourierdlem78  45712  fourierdlem81  45715  fourierdlem83  45717  fourierdlem84  45718  fourierdlem85  45719  fourierdlem87  45721  fourierdlem88  45722  fourierdlem89  45723  fourierdlem91  45725  fourierdlem92  45726  fourierdlem93  45727  fourierdlem95  45729  fourierdlem97  45731  fourierdlem101  45735  fourierdlem103  45737  fourierdlem104  45738  fourierdlem111  45745  fourierdlem112  45746  sqwvfoura  45756  sqwvfourb  45757  fouriersw  45759  elaa2lem  45761  etransclem4  45766  etransclem13  45775  etransclem35  45797  etransclem46  45808  etransclem48  45810  sge0revalmpt  45906  sge0fsummpt  45918  sge0iunmptlemfi  45941  sge0iunmptlemre  45943  sge0ltfirpmpt2  45954  sge0fsummptf  45964  nnfoctbdjlem  45983  iundjiun  45988  meaiunlelem  45996  meaiuninclem  46008  meaiuninc3v  46012  omeiunlempt  46048  carageniuncllem2  46050  caratheodorylem2  46055  0ome  46057  isomenndlem  46058  hoicvr  46076  hoicvrrex  46084  ovn0lem  46093  ovnsubaddlem1  46098  hoidmvlelem2  46124  hoidmvlelem3  46125  ovnhoilem2  46130  hoicoto2  46133  hoi2toco  46135  ovnlecvr2  46138  ovncvr2  46139  ovnsubadd2lem  46173  ovolval5lem2  46181  ovnovollem1  46184  ovnovollem2  46185  vonioolem1  46208  smfaddlem1  46291  smflimlem2  46300  smflimmpt  46338  smfinfmpt  46347  smflimsuplem2  46349  smflimsuplem4  46351  smflimsuplem5  46352  smflimsupmpt  46357  smfliminfmpt  46360  smfsupdmmbllem  46372  finfdm  46374  smfinfdmmbllem  46376  setrec2mpt  48316  aacllem  48422