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  29556  ubthlem1  30123  cnlnadjlem5  31324  xppreima2  31876  abfmpunirn  31877  aciunf1lem  31887  suppovss  31906  fpwrelmap  31958  nsgmgc  32523  xrmulc1cn  32910  esumpcvgval  33076  esumsup  33087  voliune  33227  eulerpartgbij  33371  signsplypnf  33561  iscvm  34250  mclsrcl  34552  f1omptsnlem  36217  matunitlindflem2  36485  itg2addnclem  36539  itggt0cn  36558  ftc1anclem5  36565  pwsgprod  41114  elrfirn2  41434  eq0rabdioph  41514  monotoddzz  41682  aomclem2  41797  refsumcn  43714  refsum2cnlem1  43721  fvmpt2bd  43866  fompt  43890  choicefi  43899  axccdom  43921  fvmpt4  43941  fsumsermpt  44295  fmuldfeqlem1  44298  fmuldfeq  44299  climneg  44326  climdivf  44328  mullimc  44332  idlimc  44342  sumnnodd  44346  neglimc  44363  addlimc  44364  0ellimcdiv  44365  climfveqmpt2  44409  climeqmpt  44413  limsupequzmptlem  44444  liminfvalxr  44499  xlimmnfmpt  44559  xlimpnfmpt  44560  cncfmptssg  44587  cncfshift  44590  icccncfext  44603  cncfiooicclem1  44609  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnmptdivc  44654  dvnmul  44659  dvnprodlem2  44663  itgsin0pilem1  44666  ibliccsinexp  44667  itgsinexplem1  44670  itgsinexp  44671  ditgeqiooicc  44676  itgsubsticclem  44691  itgioocnicc  44693  stoweidlem2  44718  stoweidlem11  44727  stoweidlem12  44728  stoweidlem16  44732  stoweidlem17  44733  stoweidlem18  44734  stoweidlem19  44735  stoweidlem20  44736  stoweidlem21  44737  stoweidlem22  44738  stoweidlem23  44739  stoweidlem27  44743  stoweidlem31  44747  stoweidlem34  44750  stoweidlem36  44752  stoweidlem40  44756  stoweidlem41  44757  stoweidlem42  44758  stoweidlem48  44764  stoweidlem55  44771  stoweidlem59  44775  stoweidlem62  44778  stirlinglem3  44792  stirlinglem8  44797  stirlinglem14  44803  stirlinglem15  44804  stirlingr  44806  dirkeritg  44818  dirkercncflem2  44820  fourierdlem14  44837  fourierdlem31  44854  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem56  44878  fourierdlem60  44882  fourierdlem61  44883  fourierdlem66  44888  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem77  44899  fourierdlem78  44900  fourierdlem81  44903  fourierdlem83  44905  fourierdlem84  44906  fourierdlem85  44907  fourierdlem87  44909  fourierdlem88  44910  fourierdlem89  44911  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem95  44917  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  sqwvfoura  44944  sqwvfourb  44945  fouriersw  44947  elaa2lem  44949  etransclem4  44954  etransclem13  44963  etransclem35  44985  etransclem46  44996  etransclem48  44998  sge0revalmpt  45094  sge0fsummpt  45106  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0ltfirpmpt2  45142  sge0fsummptf  45152  nnfoctbdjlem  45171  iundjiun  45176  meaiunlelem  45184  meaiuninclem  45196  meaiuninc3v  45200  omeiunlempt  45236  carageniuncllem2  45238  caratheodorylem2  45243  0ome  45245  isomenndlem  45246  hoicvr  45264  hoicvrrex  45272  ovn0lem  45281  ovnsubaddlem1  45286  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem2  45318  hoicoto2  45321  hoi2toco  45323  ovnlecvr2  45326  ovncvr2  45327  ovnsubadd2lem  45361  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  vonioolem1  45396  smfaddlem1  45479  smflimlem2  45488  smflimmpt  45526  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem4  45539  smflimsuplem5  45540  smflimsupmpt  45545  smfliminfmpt  45548  smfsupdmmbllem  45560  finfdm  45562  smfinfdmmbllem  45564  setrec2mpt  47742  aacllem  47848