Theorem fvmpt2 6959

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166   I cid 5525  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fvmptss  6960  fvmpt2d  6961  fvmptd3f  6963  mpteqb  6967  fvmptt  6968  fvmptf  6969  fnmptfvd  6993  ralrnmptw  7046  ralrnmpt  7048  fompt  7070  fmptco  7082  f1mpt  7216  offval2  7651  ofrfval2  7652  fimaproj  8085  mptelixpg  8883  dom2lem  8939  mapxpen  9081  xpmapenlem  9082  cnfcom3clem  9626  tcvalg  9657  rankf  9718  infxpenc2lem2  9942  dfac8clem  9954  acni2  9968  acnlem  9970  fin23lem32  10266  axcc2lem  10358  axcc3  10360  domtriomlem  10364  ac6num  10401  konigthlem  10491  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  seqof  14021  seqof2  14022  rlim2  15458  ello1mpt  15483  o1compt  15549  sumrblem  15673  fsumcvg  15674  summolem2a  15677  fsum  15682  fsumcvg2  15689  fsumadd  15702  isummulc2  15724  fsummulc2  15746  fsumrelem  15770  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  zprod  15902  fprod  15906  fprodmul  15925  fproddiv  15926  iserodd  16806  prmrec  16893  prdsbas3  17444  prdsdsval2  17447  invfuc  17944  yonedalem4c  18243  smndex1n0mnd  18883  gsumconst  19909  prdsgsum  19956  gsumdixp  20298  pwsgprod  20309  evlslem4  22054  elptr2  23539  ptunimpt  23560  ptcldmpt  23579  ptclsg  23580  txcnp  23585  ptcnplem  23586  cnmpt11  23628  cnmpt1t  23630  cnmptk2  23651  xkocnv  23779  flfcnp2  23972  ustn0  24186  utopsnneiplem  24212  ucnima  24245  iccpnfcnv  24911  ovolctb  25457  ovoliunlem1  25469  ovoliun2  25473  ovolshftlem1  25476  ovolscalem1  25480  voliun  25521  ioombl1lem3  25527  ioombl1lem4  25528  uniioombllem2  25550  mbfeqalem1  25608  mbfpos  25618  mbfposr  25619  mbfposb  25620  mbfsup  25631  mbfinf  25632  mbflim  25635  i1fposd  25674  itg1climres  25681  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2split  25716  itg2mono  25720  itg2cnlem1  25728  isibl2  25733  itgmpt  25750  itgeqa  25781  itggt0  25811  itgcn  25812  limcmpt  25850  dvlipcn  25961  lhop2  25982  dvfsumabs  25990  itgparts  26014  itgsubstlem  26015  itgsubst  26016  elplyd  26167  coeeulem  26189  coeeq2  26207  dvply1  26250  plyremlem  26270  ulmss  26362  ulmdvlem1  26365  mtest  26369  itgulm2  26374  radcnvlem1  26378  pserulm  26387  leibpi  26906  rlimcnp  26929  o1cxp  26938  lgamgulmlem2  26993  lgamgulmlem6  26997  lgamgulm2  26999  sqff1o  27145  lgseisenlem2  27339  dchrvmasumlem1  27458  frgrncvvdeqlem5  30373  ubthlem1  30941  cnlnadjlem5  32142  xppreima2  32724  abfmpunirn  32725  aciunf1lem  32735  suppovss  32754  fpwrelmap  32806  suppgsumssiun  33133  nsgmgc  33472  zringfrac  33614  extdgfialglem2  33837  algextdeglem6  33866  xrmulc1cn  34074  esumpcvgval  34222  esumsup  34233  voliune  34373  eulerpartgbij  34516  signsplypnf  34694  wevgblacfn  35291  iscvm  35441  mclsrcl  35743  f1omptsnlem  37652  matunitlindflem2  37938  itg2addnclem  37992  itggt0cn  38011  ftc1anclem5  38018  elrfirn2  43128  eq0rabdioph  43208  monotoddzz  43371  aomclem2  43483  refsumcn  45461  refsum2cnlem1  45468  fvmpt2bd  45600  choicefi  45629  axccdom  45651  fvmpt4  45667  fsumsermpt  46009  fmuldfeqlem1  46012  fmuldfeq  46013  climneg  46040  climdivf  46042  mullimc  46046  idlimc  46056  sumnnodd  46060  neglimc  46075  addlimc  46076  0ellimcdiv  46077  climfveqmpt2  46121  climeqmpt  46125  limsupequzmptlem  46156  liminfvalxr  46211  xlimmnfmpt  46271  xlimpnfmpt  46272  cncfmptssg  46299  cncfshift  46302  icccncfext  46315  cncfiooicclem1  46321  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmptdivc  46366  dvnmul  46371  dvnprodlem2  46375  itgsin0pilem1  46378  ibliccsinexp  46379  itgsinexplem1  46382  itgsinexp  46383  ditgeqiooicc  46388  itgsubsticclem  46403  itgioocnicc  46405  stoweidlem2  46430  stoweidlem11  46439  stoweidlem12  46440  stoweidlem16  46444  stoweidlem17  46445  stoweidlem18  46446  stoweidlem19  46447  stoweidlem20  46448  stoweidlem21  46449  stoweidlem22  46450  stoweidlem23  46451  stoweidlem27  46455  stoweidlem31  46459  stoweidlem34  46462  stoweidlem36  46464  stoweidlem40  46468  stoweidlem41  46469  stoweidlem42  46470  stoweidlem48  46476  stoweidlem55  46483  stoweidlem59  46487  stoweidlem62  46490  stirlinglem3  46504  stirlinglem8  46509  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  dirkeritg  46530  dirkercncflem2  46532  fourierdlem14  46549  fourierdlem31  46566  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem56  46590  fourierdlem60  46594  fourierdlem61  46595  fourierdlem66  46600  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem77  46611  fourierdlem78  46612  fourierdlem81  46615  fourierdlem83  46617  fourierdlem84  46618  fourierdlem85  46619  fourierdlem87  46621  fourierdlem88  46622  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  elaa2lem  46661  etransclem4  46666  etransclem13  46675  etransclem35  46697  etransclem46  46708  etransclem48  46710  sge0revalmpt  46806  sge0fsummpt  46818  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0ltfirpmpt2  46854  sge0fsummptf  46864  nnfoctbdjlem  46883  iundjiun  46888  meaiunlelem  46896  meaiuninclem  46908  meaiuninc3v  46912  omeiunlempt  46948  carageniuncllem2  46950  caratheodorylem2  46955  0ome  46957  isomenndlem  46958  hoicvr  46976  hoicvrrex  46984  ovn0lem  46993  ovnsubaddlem1  46998  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem2  47030  hoicoto2  47033  hoi2toco  47035  ovnlecvr2  47038  ovncvr2  47039  ovnsubadd2lem  47073  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  vonioolem1  47108  smfaddlem1  47191  smflimlem2  47200  smflimmpt  47238  smflimsuplem2  47249  smflimsuplem4  47251  smflimsuplem5  47252  smflimsupmpt  47257  smfliminfmpt  47260  smfsupdmmbllem  47272  finfdm  47274  smfinfdmmbllem  47276  setrec2mpt  50172  aacllem  50276