Theorem fvmpt2 7010

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5232   I cid 5574  ‘cfv 6544

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fv 6552

This theorem is referenced by:  fvmptss  7011  fvmpt2d  7012  fvmptd3f  7014  mpteqb  7018  fvmptt  7019  fvmptf  7020  fnmptfvd  7043  ralrnmptw  7096  ralrnmpt  7098  fmptco  7127  f1mpt  7260  offval2  7690  ofrfval2  7691  fimaproj  8121  mptelixpg  8929  dom2lem  8988  mapxpen  9143  xpmapenlem  9144  cnfcom3clem  9700  tcvalg  9733  rankf  9789  infxpenc2lem2  10015  dfac8clem  10027  acni2  10041  acnlem  10043  fin23lem32  10339  axcc2lem  10431  axcc3  10433  domtriomlem  10437  ac6num  10474  konigthlem  10563  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  seqof  14025  seqof2  14026  rlim2  15440  ello1mpt  15465  o1compt  15531  sumrblem  15657  fsumcvg  15658  summolem2a  15661  fsum  15666  fsumcvg2  15673  fsumadd  15686  isummulc2  15708  fsummulc2  15730  fsumrelem  15753  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  fprod  15885  fprodmul  15904  fproddiv  15905  iserodd  16768  prmrec  16855  prdsbas3  17427  prdsdsval2  17430  invfuc  17927  yonedalem4c  18230  smndex1n0mnd  18793  gsumconst  19802  prdsgsum  19849  gsumdixp  20131  evlslem4  21637  elptr2  23078  ptunimpt  23099  ptcldmpt  23118  ptclsg  23119  txcnp  23124  ptcnplem  23125  cnmpt11  23167  cnmpt1t  23169  cnmptk2  23190  xkocnv  23318  flfcnp2  23511  ustn0  23725  utopsnneiplem  23752  ucnima  23786  iccpnfcnv  24460  ovolctb  25007  ovoliunlem1  25019  ovoliun2  25023  ovolshftlem1  25026  ovolscalem1  25030  voliun  25071  ioombl1lem3  25077  ioombl1lem4  25078  uniioombllem2  25100  mbfeqalem1  25158  mbfpos  25168  mbfposr  25169  mbfposb  25170  mbfsup  25181  mbfinf  25182  mbflim  25185  i1fposd  25225  itg1climres  25232  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  itg2split  25267  itg2mono  25271  itg2cnlem1  25279  isibl2  25284  itgmpt  25300  itgeqa  25331  itggt0  25361  itgcn  25362  limcmpt  25400  dvlipcn  25511  lhop2  25532  dvfsumabs  25540  itgparts  25564  itgsubstlem  25565  itgsubst  25566  elplyd  25716  coeeulem  25738  coeeq2  25756  dvply1  25797  plyremlem  25817  ulmss  25909  ulmdvlem1  25912  mtest  25916  itgulm2  25921  radcnvlem1  25925  pserulm  25934  leibpi  26447  rlimcnp  26470  o1cxp  26479  lgamgulmlem2  26534  lgamgulmlem6  26538  lgamgulm2  26540  sqff1o  26686  lgseisenlem2  26879  dchrvmasumlem1  26998  frgrncvvdeqlem5  29587  ubthlem1  30154  cnlnadjlem5  31355  xppreima2  31907  abfmpunirn  31908  aciunf1lem  31918  suppovss  31937  fpwrelmap  31989  nsgmgc  32554  xrmulc1cn  32941  esumpcvgval  33107  esumsup  33118  voliune  33258  eulerpartgbij  33402  signsplypnf  33592  iscvm  34281  mclsrcl  34583  f1omptsnlem  36265  matunitlindflem2  36533  itg2addnclem  36587  itggt0cn  36606  ftc1anclem5  36613  pwsgprod  41162  elrfirn2  41482  eq0rabdioph  41562  monotoddzz  41730  aomclem2  41845  refsumcn  43762  refsum2cnlem1  43769  fvmpt2bd  43914  fompt  43938  choicefi  43947  axccdom  43969  fvmpt4  43989  fsumsermpt  44343  fmuldfeqlem1  44346  fmuldfeq  44347  climneg  44374  climdivf  44376  mullimc  44380  idlimc  44390  sumnnodd  44394  neglimc  44411  addlimc  44412  0ellimcdiv  44413  climfveqmpt2  44457  climeqmpt  44461  limsupequzmptlem  44492  liminfvalxr  44547  xlimmnfmpt  44607  xlimpnfmpt  44608  cncfmptssg  44635  cncfshift  44638  icccncfext  44651  cncfiooicclem1  44657  fprodsubrecnncnvlem  44671  fprodaddrecnncnvlem  44673  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvnmptdivc  44702  dvnmul  44707  dvnprodlem2  44711  itgsin0pilem1  44714  ibliccsinexp  44715  itgsinexplem1  44718  itgsinexp  44719  ditgeqiooicc  44724  itgsubsticclem  44739  itgioocnicc  44741  stoweidlem2  44766  stoweidlem11  44775  stoweidlem12  44776  stoweidlem16  44780  stoweidlem17  44781  stoweidlem18  44782  stoweidlem19  44783  stoweidlem20  44784  stoweidlem21  44785  stoweidlem22  44786  stoweidlem23  44787  stoweidlem27  44791  stoweidlem31  44795  stoweidlem34  44798  stoweidlem36  44800  stoweidlem40  44804  stoweidlem41  44805  stoweidlem42  44806  stoweidlem48  44812  stoweidlem55  44819  stoweidlem59  44823  stoweidlem62  44826  stirlinglem3  44840  stirlinglem8  44845  stirlinglem14  44851  stirlinglem15  44852  stirlingr  44854  dirkeritg  44866  dirkercncflem2  44868  fourierdlem14  44885  fourierdlem31  44902  fourierdlem41  44912  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  fourierdlem51  44921  fourierdlem56  44926  fourierdlem60  44930  fourierdlem61  44931  fourierdlem66  44936  fourierdlem70  44940  fourierdlem71  44941  fourierdlem73  44943  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem77  44947  fourierdlem78  44948  fourierdlem81  44951  fourierdlem83  44953  fourierdlem84  44954  fourierdlem85  44955  fourierdlem87  44957  fourierdlem88  44958  fourierdlem89  44959  fourierdlem91  44961  fourierdlem92  44962  fourierdlem93  44963  fourierdlem95  44965  fourierdlem97  44967  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  fourierdlem111  44981  fourierdlem112  44982  sqwvfoura  44992  sqwvfourb  44993  fouriersw  44995  elaa2lem  44997  etransclem4  45002  etransclem13  45011  etransclem35  45033  etransclem46  45044  etransclem48  45046  sge0revalmpt  45142  sge0fsummpt  45154  sge0iunmptlemfi  45177  sge0iunmptlemre  45179  sge0ltfirpmpt2  45190  sge0fsummptf  45200  nnfoctbdjlem  45219  iundjiun  45224  meaiunlelem  45232  meaiuninclem  45244  meaiuninc3v  45248  omeiunlempt  45284  carageniuncllem2  45286  caratheodorylem2  45291  0ome  45293  isomenndlem  45294  hoicvr  45312  hoicvrrex  45320  ovn0lem  45329  ovnsubaddlem1  45334  hoidmvlelem2  45360  hoidmvlelem3  45361  ovnhoilem2  45366  hoicoto2  45369  hoi2toco  45371  ovnlecvr2  45374  ovncvr2  45375  ovnsubadd2lem  45409  ovolval5lem2  45417  ovnovollem1  45420  ovnovollem2  45421  vonioolem1  45444  smfaddlem1  45527  smflimlem2  45536  smflimmpt  45574  smfinfmpt  45583  smflimsuplem2  45585  smflimsuplem4  45587  smflimsuplem5  45588  smflimsupmpt  45593  smfliminfmpt  45596  smfsupdmmbllem  45608  finfdm  45610  smfinfdmmbllem  45612  setrec2mpt  47790  aacllem  47896