Theorem fvmpt2 6983

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5180   I cid 5539  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fv 6525

This theorem is referenced by:  fvmptss  6984  fvmpt2d  6985  fvmptd3f  6987  mpteqb  6991  fvmptt  6992  fvmptf  6993  fnmptfvd  7018  ralrnmptw  7071  ralrnmpt  7073  fompt  7095  fmptco  7107  f1mpt  7241  offval2  7676  ofrfval2  7677  fimaproj  8110  mptelixpg  8913  dom2lem  8969  mapxpen  9111  xpmapenlem  9112  cnfcom3clem  9657  tcvalg  9688  rankf  9749  infxpenc2lem2  9973  dfac8clem  9985  acni2  9999  acnlem  10001  fin23lem32  10298  axcc2lem  10390  axcc3  10392  domtriomlem  10396  ac6num  10433  konigthlem  10523  rpnnen1lem1  12976  rpnnen1lem3  12977  rpnnen1lem5  12979  seqof  14069  seqof2  14070  rlim2  15506  ello1mpt  15531  o1compt  15597  sumrblem  15721  fsumcvg  15722  summolem2a  15725  fsum  15730  fsumcvg2  15737  fsumadd  15750  isummulc2  15772  fsummulc2  15794  fsumrelem  15818  prodrblem  15942  fprodcvg  15943  prodmolem2a  15947  zprod  15950  fprod  15954  fprodmul  15973  fproddiv  15974  iserodd  16854  prmrec  16941  prdsbas3  17493  prdsdsval2  17496  invfuc  17993  yonedalem4c  18292  smndex1n0mnd  18932  gsumconst  19957  prdsgsum  20004  gsumdixp  20346  pwsgprod  20357  evlslem4  22109  elptr2  23614  ptunimpt  23635  ptcldmpt  23654  ptclsg  23655  txcnp  23660  ptcnplem  23661  cnmpt11  23703  cnmpt1t  23705  cnmptk2  23726  xkocnv  23854  flfcnp2  24047  ustn0  24261  utopsnneiplem  24287  ucnima  24320  iccpnfcnv  24986  ovolctb  25532  ovoliunlem1  25544  ovoliun2  25548  ovolshftlem1  25551  ovolscalem1  25555  voliun  25596  ioombl1lem3  25602  ioombl1lem4  25603  uniioombllem2  25625  mbfeqalem1  25683  mbfpos  25693  mbfposr  25694  mbfposb  25695  mbfsup  25706  mbfinf  25707  mbflim  25710  i1fposd  25749  itg1climres  25756  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mbfi1fseqlem6  25762  itg2split  25791  itg2mono  25795  itg2cnlem1  25803  isibl2  25808  itgmpt  25825  itgeqa  25856  itggt0  25886  itgcn  25887  limcmpt  25925  dvlipcn  26036  lhop2  26057  dvfsumabs  26065  itgparts  26089  itgsubstlem  26090  itgsubst  26091  elplyd  26242  coeeulem  26264  coeeq2  26282  dvply1  26325  plyremlem  26345  ulmss  26437  ulmdvlem1  26440  mtest  26444  itgulm2  26449  radcnvlem1  26453  pserulm  26462  leibpi  26984  rlimcnp  27007  o1cxp  27016  lgamgulmlem2  27071  lgamgulmlem6  27075  lgamgulm2  27077  sqff1o  27223  lgseisenlem2  27417  dchrvmasumlem1  27536  frgrncvvdeqlem5  30451  ubthlem1  31019  cnlnadjlem5  32220  xppreima2  32803  abfmpunirn  32804  aciunf1lem  32814  suppovss  32833  fpwrelmap  32885  suppgsumssiun  33213  nsgmgc  33559  zringfrac  33711  extdgfialglem2  33951  algextdeglem6  33980  xrmulc1cn  34188  esumpcvgval  34336  esumsup  34347  voliune  34487  eulerpartgbij  34630  signsplypnf  34808  wevgblacfn  35418  iscvm  35573  mclsrcl  35875  f1omptsnlem  37794  matunitlindflem2  38080  itg2addnclem  38134  itggt0cn  38153  ftc1anclem5  38160  elrfirn2  43241  eq0rabdioph  43321  monotoddzz  43484  aomclem2  43596  refsumcn  45574  refsum2cnlem1  45581  fvmpt2bd  45712  choicefi  45741  axccdom  45762  fvmpt4  45777  fsumsermpt  46119  fmuldfeqlem1  46122  fmuldfeq  46123  climneg  46150  climdivf  46152  mullimc  46156  idlimc  46166  sumnnodd  46170  neglimc  46185  addlimc  46186  0ellimcdiv  46187  climfveqmpt2  46231  climeqmpt  46235  limsupequzmptlem  46266  liminfvalxr  46321  xlimmnfmpt  46381  xlimpnfmpt  46382  cncfmptssg  46409  cncfshift  46412  icccncfext  46425  cncfiooicclem1  46431  fprodsubrecnncnvlem  46445  fprodaddrecnncnvlem  46447  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnmptdivc  46476  dvnmul  46481  dvnprodlem2  46485  itgsin0pilem1  46488  ibliccsinexp  46489  itgsinexplem1  46492  itgsinexp  46493  ditgeqiooicc  46498  itgsubsticclem  46513  itgioocnicc  46515  stoweidlem2  46540  stoweidlem11  46549  stoweidlem12  46550  stoweidlem16  46554  stoweidlem17  46555  stoweidlem18  46556  stoweidlem19  46557  stoweidlem20  46558  stoweidlem21  46559  stoweidlem22  46560  stoweidlem23  46561  stoweidlem27  46565  stoweidlem31  46569  stoweidlem34  46572  stoweidlem36  46574  stoweidlem40  46578  stoweidlem41  46579  stoweidlem42  46580  stoweidlem48  46586  stoweidlem55  46593  stoweidlem59  46597  stoweidlem62  46600  stirlinglem3  46614  stirlinglem8  46619  stirlinglem14  46625  stirlinglem15  46626  stirlingr  46628  dirkeritg  46640  dirkercncflem2  46642  fourierdlem14  46659  fourierdlem31  46676  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem51  46695  fourierdlem56  46700  fourierdlem60  46704  fourierdlem61  46705  fourierdlem66  46710  fourierdlem70  46714  fourierdlem71  46715  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem77  46721  fourierdlem78  46722  fourierdlem81  46725  fourierdlem83  46727  fourierdlem84  46728  fourierdlem85  46729  fourierdlem87  46731  fourierdlem88  46732  fourierdlem89  46733  fourierdlem91  46735  fourierdlem92  46736  fourierdlem93  46737  fourierdlem95  46739  fourierdlem97  46741  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem112  46756  sqwvfoura  46766  sqwvfourb  46767  fouriersw  46769  elaa2lem  46771  etransclem4  46776  etransclem13  46785  etransclem35  46807  etransclem46  46818  etransclem48  46820  sge0revalmpt  46916  sge0fsummpt  46928  sge0iunmptlemfi  46951  sge0iunmptlemre  46953  sge0ltfirpmpt2  46964  sge0fsummptf  46974  nnfoctbdjlem  46993  iundjiun  46998  meaiunlelem  47006  meaiuninclem  47018  meaiuninc3v  47022  omeiunlempt  47058  carageniuncllem2  47060  caratheodorylem2  47065  0ome  47067  isomenndlem  47068  hoicvr  47086  hoicvrrex  47094  ovn0lem  47103  ovnsubaddlem1  47108  hoidmvlelem2  47134  hoidmvlelem3  47135  ovnhoilem2  47140  hoicoto2  47143  hoi2toco  47145  ovnlecvr2  47148  ovncvr2  47149  ovnsubadd2lem  47183  ovolval5lem2  47191  ovnovollem1  47194  ovnovollem2  47195  vonioolem1  47218  smfaddlem1  47301  smflimlem2  47310  smflimmpt  47348  smflimsuplem2  47359  smflimsuplem4  47361  smflimsuplem5  47362  smflimsupmpt  47367  smfliminfmpt  47370  smfsupdmmbllem  47382  finfdm  47384  smfinfdmmbllem  47386  setrec2mpt  50282  aacllem  50386