Theorem fvmpt2 7007

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ↦ cmpt 5205   I cid 5557  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fv 6549

This theorem is referenced by:  fvmptss  7008  fvmpt2d  7009  fvmptd3f  7011  mpteqb  7015  fvmptt  7016  fvmptf  7017  fnmptfvd  7041  ralrnmptw  7094  ralrnmpt  7096  fompt  7118  fmptco  7129  f1mpt  7263  offval2  7699  ofrfval2  7700  fimaproj  8142  mptelixpg  8957  dom2lem  9014  mapxpen  9165  xpmapenlem  9166  cnfcom3clem  9727  tcvalg  9760  rankf  9816  infxpenc2lem2  10042  dfac8clem  10054  acni2  10068  acnlem  10070  fin23lem32  10366  axcc2lem  10458  axcc3  10460  domtriomlem  10464  ac6num  10501  konigthlem  10590  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  seqof  14082  seqof2  14083  rlim2  15515  ello1mpt  15540  o1compt  15606  sumrblem  15730  fsumcvg  15731  summolem2a  15734  fsum  15739  fsumcvg2  15746  fsumadd  15759  isummulc2  15781  fsummulc2  15803  fsumrelem  15826  prodrblem  15948  fprodcvg  15949  prodmolem2a  15953  zprod  15956  fprod  15960  fprodmul  15979  fproddiv  15980  iserodd  16856  prmrec  16943  prdsbas3  17498  prdsdsval2  17501  invfuc  17994  yonedalem4c  18293  smndex1n0mnd  18895  gsumconst  19921  prdsgsum  19968  gsumdixp  20285  evlslem4  22049  elptr2  23529  ptunimpt  23550  ptcldmpt  23569  ptclsg  23570  txcnp  23575  ptcnplem  23576  cnmpt11  23618  cnmpt1t  23620  cnmptk2  23641  xkocnv  23769  flfcnp2  23962  ustn0  24176  utopsnneiplem  24203  ucnima  24236  iccpnfcnv  24912  ovolctb  25462  ovoliunlem1  25474  ovoliun2  25478  ovolshftlem1  25481  ovolscalem1  25485  voliun  25526  ioombl1lem3  25532  ioombl1lem4  25533  uniioombllem2  25555  mbfeqalem1  25613  mbfpos  25623  mbfposr  25624  mbfposb  25625  mbfsup  25636  mbfinf  25637  mbflim  25640  i1fposd  25679  itg1climres  25686  mbfi1fseqlem4  25690  mbfi1fseqlem5  25691  mbfi1fseqlem6  25692  itg2split  25721  itg2mono  25725  itg2cnlem1  25733  isibl2  25738  itgmpt  25755  itgeqa  25786  itggt0  25816  itgcn  25817  limcmpt  25855  dvlipcn  25970  lhop2  25991  dvfsumabs  26000  itgparts  26025  itgsubstlem  26026  itgsubst  26027  elplyd  26178  coeeulem  26200  coeeq2  26218  dvply1  26262  plyremlem  26283  ulmss  26377  ulmdvlem1  26380  mtest  26384  itgulm2  26389  radcnvlem1  26393  pserulm  26402  leibpi  26922  rlimcnp  26945  o1cxp  26955  lgamgulmlem2  27010  lgamgulmlem6  27014  lgamgulm2  27016  sqff1o  27162  lgseisenlem2  27357  dchrvmasumlem1  27476  frgrncvvdeqlem5  30251  ubthlem1  30818  cnlnadjlem5  32019  xppreima2  32597  abfmpunirn  32598  aciunf1lem  32608  suppovss  32626  fpwrelmap  32680  nsgmgc  33380  zringfrac  33522  algextdeglem6  33707  xrmulc1cn  33904  esumpcvgval  34054  esumsup  34065  voliune  34205  eulerpartgbij  34349  signsplypnf  34540  wevgblacfn  35089  iscvm  35239  mclsrcl  35541  f1omptsnlem  37312  matunitlindflem2  37599  itg2addnclem  37653  itggt0cn  37672  ftc1anclem5  37679  pwsgprod  42533  elrfirn2  42685  eq0rabdioph  42765  monotoddzz  42933  aomclem2  43045  refsumcn  45007  refsum2cnlem1  45014  fvmpt2bd  45147  choicefi  45177  axccdom  45199  fvmpt4  45216  fsumsermpt  45566  fmuldfeqlem1  45569  fmuldfeq  45570  climneg  45597  climdivf  45599  mullimc  45603  idlimc  45613  sumnnodd  45617  neglimc  45634  addlimc  45635  0ellimcdiv  45636  climfveqmpt2  45680  climeqmpt  45684  limsupequzmptlem  45715  liminfvalxr  45770  xlimmnfmpt  45830  xlimpnfmpt  45831  cncfmptssg  45858  cncfshift  45861  icccncfext  45874  cncfiooicclem1  45880  fprodsubrecnncnvlem  45894  fprodaddrecnncnvlem  45896  ioodvbdlimc1lem2  45919  ioodvbdlimc2lem  45921  dvnmptdivc  45925  dvnmul  45930  dvnprodlem2  45934  itgsin0pilem1  45937  ibliccsinexp  45938  itgsinexplem1  45941  itgsinexp  45942  ditgeqiooicc  45947  itgsubsticclem  45962  itgioocnicc  45964  stoweidlem2  45989  stoweidlem11  45998  stoweidlem12  45999  stoweidlem16  46003  stoweidlem17  46004  stoweidlem18  46005  stoweidlem19  46006  stoweidlem20  46007  stoweidlem21  46008  stoweidlem22  46009  stoweidlem23  46010  stoweidlem27  46014  stoweidlem31  46018  stoweidlem34  46021  stoweidlem36  46023  stoweidlem40  46027  stoweidlem41  46028  stoweidlem42  46029  stoweidlem48  46035  stoweidlem55  46042  stoweidlem59  46046  stoweidlem62  46049  stirlinglem3  46063  stirlinglem8  46068  stirlinglem14  46074  stirlinglem15  46075  stirlingr  46077  dirkeritg  46089  dirkercncflem2  46091  fourierdlem14  46108  fourierdlem31  46125  fourierdlem41  46135  fourierdlem48  46141  fourierdlem49  46142  fourierdlem50  46143  fourierdlem51  46144  fourierdlem56  46149  fourierdlem60  46153  fourierdlem61  46154  fourierdlem66  46159  fourierdlem70  46163  fourierdlem71  46164  fourierdlem73  46166  fourierdlem74  46167  fourierdlem75  46168  fourierdlem76  46169  fourierdlem77  46170  fourierdlem78  46171  fourierdlem81  46174  fourierdlem83  46176  fourierdlem84  46177  fourierdlem85  46178  fourierdlem87  46180  fourierdlem88  46181  fourierdlem89  46182  fourierdlem91  46184  fourierdlem92  46185  fourierdlem93  46186  fourierdlem95  46188  fourierdlem97  46190  fourierdlem101  46194  fourierdlem103  46196  fourierdlem104  46197  fourierdlem111  46204  fourierdlem112  46205  sqwvfoura  46215  sqwvfourb  46216  fouriersw  46218  elaa2lem  46220  etransclem4  46225  etransclem13  46234  etransclem35  46256  etransclem46  46267  etransclem48  46269  sge0revalmpt  46365  sge0fsummpt  46377  sge0iunmptlemfi  46400  sge0iunmptlemre  46402  sge0ltfirpmpt2  46413  sge0fsummptf  46423  nnfoctbdjlem  46442  iundjiun  46447  meaiunlelem  46455  meaiuninclem  46467  meaiuninc3v  46471  omeiunlempt  46507  carageniuncllem2  46509  caratheodorylem2  46514  0ome  46516  isomenndlem  46517  hoicvr  46535  hoicvrrex  46543  ovn0lem  46552  ovnsubaddlem1  46557  hoidmvlelem2  46583  hoidmvlelem3  46584  ovnhoilem2  46589  hoicoto2  46592  hoi2toco  46594  ovnlecvr2  46597  ovncvr2  46598  ovnsubadd2lem  46632  ovolval5lem2  46640  ovnovollem1  46643  ovnovollem2  46644  vonioolem1  46667  smfaddlem1  46750  smflimlem2  46759  smflimmpt  46797  smflimsuplem2  46808  smflimsuplem4  46810  smflimsuplem5  46811  smflimsupmpt  46816  smfliminfmpt  46819  smfsupdmmbllem  46831  finfdm  46833  smfinfdmmbllem  46835  setrec2mpt  49311  aacllem  49415