Theorem fvmpt2 6868

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153   I cid 5479  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvmptss  6869  fvmpt2d  6870  fvmptd3f  6872  mpteqb  6876  fvmptt  6877  fvmptf  6878  fnmptfvd  6900  ralrnmptw  6952  ralrnmpt  6954  fmptco  6983  f1mpt  7115  offval2  7531  ofrfval2  7532  fimaproj  7947  mptelixpg  8681  dom2lem  8735  mapxpen  8879  xpmapenlem  8880  cnfcom3clem  9393  tcvalg  9427  rankf  9483  infxpenc2lem2  9707  dfac8clem  9719  acni2  9733  acnlem  9735  fin23lem32  10031  axcc2lem  10123  axcc3  10125  domtriomlem  10129  ac6num  10166  konigthlem  10255  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  seqof  13708  seqof2  13709  rlim2  15133  ello1mpt  15158  o1compt  15224  sumrblem  15351  fsumcvg  15352  summolem2a  15355  fsum  15360  fsumcvg2  15367  fsumadd  15380  isummulc2  15402  fsummulc2  15424  fsumrelem  15447  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  zprod  15575  fprod  15579  fprodmul  15598  fproddiv  15599  iserodd  16464  prmrec  16551  prdsbas3  17109  prdsdsval2  17112  invfuc  17608  yonedalem4c  17911  smndex1n0mnd  18466  gsumconst  19450  prdsgsum  19497  gsumdixp  19763  evlslem4  21194  elptr2  22633  ptunimpt  22654  ptcldmpt  22673  ptclsg  22674  txcnp  22679  ptcnplem  22680  cnmpt11  22722  cnmpt1t  22724  cnmptk2  22745  xkocnv  22873  flfcnp2  23066  ustn0  23280  utopsnneiplem  23307  ucnima  23341  iccpnfcnv  24013  ovolctb  24559  ovoliunlem1  24571  ovoliun2  24575  ovolshftlem1  24578  ovolscalem1  24582  voliun  24623  ioombl1lem3  24629  ioombl1lem4  24630  uniioombllem2  24652  mbfeqalem1  24710  mbfpos  24720  mbfposr  24721  mbfposb  24722  mbfsup  24733  mbfinf  24734  mbflim  24737  i1fposd  24777  itg1climres  24784  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2split  24819  itg2mono  24823  itg2cnlem1  24831  isibl2  24836  itgmpt  24852  itgeqa  24883  itggt0  24913  itgcn  24914  limcmpt  24952  dvlipcn  25063  lhop2  25084  dvfsumabs  25092  itgparts  25116  itgsubstlem  25117  itgsubst  25118  elplyd  25268  coeeulem  25290  coeeq2  25308  dvply1  25349  plyremlem  25369  ulmss  25461  ulmdvlem1  25464  mtest  25468  itgulm2  25473  radcnvlem1  25477  pserulm  25486  leibpi  25997  rlimcnp  26020  o1cxp  26029  lgamgulmlem2  26084  lgamgulmlem6  26088  lgamgulm2  26090  sqff1o  26236  lgseisenlem2  26429  dchrvmasumlem1  26548  frgrncvvdeqlem5  28568  ubthlem1  29133  cnlnadjlem5  30334  xppreima2  30889  abfmpunirn  30891  aciunf1lem  30901  suppovss  30919  fpwrelmap  30970  nsgmgc  31499  xrmulc1cn  31782  esumpcvgval  31946  esumsup  31957  voliune  32097  eulerpartgbij  32239  signsplypnf  32429  iscvm  33121  mclsrcl  33423  f1omptsnlem  35434  matunitlindflem2  35701  itg2addnclem  35755  itggt0cn  35774  ftc1anclem5  35781  pwsgprod  40194  elrfirn2  40434  eq0rabdioph  40514  monotoddzz  40681  aomclem2  40796  refsumcn  42462  refsum2cnlem1  42469  fvmpt2bd  42595  fompt  42619  choicefi  42629  axccdom  42651  fvmpt4  42671  fsumsermpt  43010  fmuldfeqlem1  43013  fmuldfeq  43014  climneg  43041  climdivf  43043  mullimc  43047  idlimc  43057  sumnnodd  43061  neglimc  43078  addlimc  43079  0ellimcdiv  43080  climfveqmpt2  43124  climeqmpt  43128  limsupequzmptlem  43159  liminfvalxr  43214  xlimmnfmpt  43274  xlimpnfmpt  43275  cncfmptssg  43302  cncfshift  43305  icccncfext  43318  cncfiooicclem1  43324  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmptdivc  43369  dvnmul  43374  dvnprodlem2  43378  itgsin0pilem1  43381  ibliccsinexp  43382  itgsinexplem1  43385  itgsinexp  43386  ditgeqiooicc  43391  itgsubsticclem  43406  itgioocnicc  43408  stoweidlem2  43433  stoweidlem11  43442  stoweidlem12  43443  stoweidlem16  43447  stoweidlem17  43448  stoweidlem18  43449  stoweidlem19  43450  stoweidlem20  43451  stoweidlem21  43452  stoweidlem22  43453  stoweidlem23  43454  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  stoweidlem36  43467  stoweidlem40  43471  stoweidlem41  43472  stoweidlem42  43473  stoweidlem48  43479  stoweidlem55  43486  stoweidlem59  43490  stoweidlem62  43493  stirlinglem3  43507  stirlinglem8  43512  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  dirkeritg  43533  dirkercncflem2  43535  fourierdlem14  43552  fourierdlem31  43569  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem56  43593  fourierdlem60  43597  fourierdlem61  43598  fourierdlem66  43603  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem77  43614  fourierdlem78  43615  fourierdlem81  43618  fourierdlem83  43620  fourierdlem84  43621  fourierdlem85  43622  fourierdlem87  43624  fourierdlem88  43625  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem95  43632  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  elaa2lem  43664  etransclem4  43669  etransclem13  43678  etransclem35  43700  etransclem46  43711  etransclem48  43713  sge0revalmpt  43806  sge0fsummpt  43818  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0ltfirpmpt2  43854  sge0fsummptf  43864  nnfoctbdjlem  43883  iundjiun  43888  meaiunlelem  43896  meaiuninclem  43908  meaiuninc3v  43912  omeiunlempt  43948  carageniuncllem2  43950  caratheodorylem2  43955  0ome  43957  isomenndlem  43958  hoicvr  43976  hoicvrrex  43984  ovn0lem  43993  ovnsubaddlem1  43998  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem2  44030  hoicoto2  44033  hoi2toco  44035  ovnlecvr2  44038  ovncvr2  44039  ovnsubadd2lem  44073  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  vonioolem1  44108  smfaddlem1  44185  smflimlem2  44194  smflimmpt  44230  smfinfmpt  44239  smflimsuplem2  44241  smflimsuplem4  44243  smflimsuplem5  44244  smflimsupmpt  44249  smfliminfmpt  44252  aacllem  46391