Theorem fvmpt2 7040

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249   I cid 5592  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  fvmptss  7041  fvmpt2d  7042  fvmptd3f  7044  mpteqb  7048  fvmptt  7049  fvmptf  7050  fnmptfvd  7074  ralrnmptw  7128  ralrnmpt  7130  fompt  7152  fmptco  7163  f1mpt  7298  offval2  7734  ofrfval2  7735  fimaproj  8176  mptelixpg  8993  dom2lem  9052  mapxpen  9209  xpmapenlem  9210  cnfcom3clem  9774  tcvalg  9807  rankf  9863  infxpenc2lem2  10089  dfac8clem  10101  acni2  10115  acnlem  10117  fin23lem32  10413  axcc2lem  10505  axcc3  10507  domtriomlem  10511  ac6num  10548  konigthlem  10637  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  seqof  14110  seqof2  14111  rlim2  15542  ello1mpt  15567  o1compt  15633  sumrblem  15759  fsumcvg  15760  summolem2a  15763  fsum  15768  fsumcvg2  15775  fsumadd  15788  isummulc2  15810  fsummulc2  15832  fsumrelem  15855  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  fprod  15989  fprodmul  16008  fproddiv  16009  iserodd  16882  prmrec  16969  prdsbas3  17541  prdsdsval2  17544  invfuc  18044  yonedalem4c  18347  smndex1n0mnd  18947  gsumconst  19976  prdsgsum  20023  gsumdixp  20342  evlslem4  22123  elptr2  23603  ptunimpt  23624  ptcldmpt  23643  ptclsg  23644  txcnp  23649  ptcnplem  23650  cnmpt11  23692  cnmpt1t  23694  cnmptk2  23715  xkocnv  23843  flfcnp2  24036  ustn0  24250  utopsnneiplem  24277  ucnima  24311  iccpnfcnv  24994  ovolctb  25544  ovoliunlem1  25556  ovoliun2  25560  ovolshftlem1  25563  ovolscalem1  25567  voliun  25608  ioombl1lem3  25614  ioombl1lem4  25615  uniioombllem2  25637  mbfeqalem1  25695  mbfpos  25705  mbfposr  25706  mbfposb  25707  mbfsup  25718  mbfinf  25719  mbflim  25722  i1fposd  25762  itg1climres  25769  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2split  25804  itg2mono  25808  itg2cnlem1  25816  isibl2  25821  itgmpt  25838  itgeqa  25869  itggt0  25899  itgcn  25900  limcmpt  25938  dvlipcn  26053  lhop2  26074  dvfsumabs  26083  itgparts  26108  itgsubstlem  26109  itgsubst  26110  elplyd  26261  coeeulem  26283  coeeq2  26301  dvply1  26343  plyremlem  26364  ulmss  26458  ulmdvlem1  26461  mtest  26465  itgulm2  26470  radcnvlem1  26474  pserulm  26483  leibpi  27003  rlimcnp  27026  o1cxp  27036  lgamgulmlem2  27091  lgamgulmlem6  27095  lgamgulm2  27097  sqff1o  27243  lgseisenlem2  27438  dchrvmasumlem1  27557  frgrncvvdeqlem5  30335  ubthlem1  30902  cnlnadjlem5  32103  xppreima2  32669  abfmpunirn  32670  aciunf1lem  32680  suppovss  32697  fpwrelmap  32747  nsgmgc  33405  zringfrac  33547  algextdeglem6  33713  xrmulc1cn  33876  esumpcvgval  34042  esumsup  34053  voliune  34193  eulerpartgbij  34337  signsplypnf  34527  wevgblacfn  35076  iscvm  35227  mclsrcl  35529  f1omptsnlem  37302  matunitlindflem2  37577  itg2addnclem  37631  itggt0cn  37650  ftc1anclem5  37657  pwsgprod  42499  elrfirn2  42652  eq0rabdioph  42732  monotoddzz  42900  aomclem2  43012  refsumcn  44930  refsum2cnlem1  44937  fvmpt2bd  45077  choicefi  45107  axccdom  45129  fvmpt4  45146  fsumsermpt  45500  fmuldfeqlem1  45503  fmuldfeq  45504  climneg  45531  climdivf  45533  mullimc  45537  idlimc  45547  sumnnodd  45551  neglimc  45568  addlimc  45569  0ellimcdiv  45570  climfveqmpt2  45614  climeqmpt  45618  limsupequzmptlem  45649  liminfvalxr  45704  xlimmnfmpt  45764  xlimpnfmpt  45765  cncfmptssg  45792  cncfshift  45795  icccncfext  45808  cncfiooicclem1  45814  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmptdivc  45859  dvnmul  45864  dvnprodlem2  45868  itgsin0pilem1  45871  ibliccsinexp  45872  itgsinexplem1  45875  itgsinexp  45876  ditgeqiooicc  45881  itgsubsticclem  45896  itgioocnicc  45898  stoweidlem2  45923  stoweidlem11  45932  stoweidlem12  45933  stoweidlem16  45937  stoweidlem17  45938  stoweidlem18  45939  stoweidlem19  45940  stoweidlem20  45941  stoweidlem21  45942  stoweidlem22  45943  stoweidlem23  45944  stoweidlem27  45948  stoweidlem31  45952  stoweidlem34  45955  stoweidlem36  45957  stoweidlem40  45961  stoweidlem41  45962  stoweidlem42  45963  stoweidlem48  45969  stoweidlem55  45976  stoweidlem59  45980  stoweidlem62  45983  stirlinglem3  45997  stirlinglem8  46002  stirlinglem14  46008  stirlinglem15  46009  stirlingr  46011  dirkeritg  46023  dirkercncflem2  46025  fourierdlem14  46042  fourierdlem31  46059  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem56  46083  fourierdlem60  46087  fourierdlem61  46088  fourierdlem66  46093  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem77  46104  fourierdlem78  46105  fourierdlem81  46108  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem87  46114  fourierdlem88  46115  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  elaa2lem  46154  etransclem4  46159  etransclem13  46168  etransclem35  46190  etransclem46  46201  etransclem48  46203  sge0revalmpt  46299  sge0fsummpt  46311  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0ltfirpmpt2  46347  sge0fsummptf  46357  nnfoctbdjlem  46376  iundjiun  46381  meaiunlelem  46389  meaiuninclem  46401  meaiuninc3v  46405  omeiunlempt  46441  carageniuncllem2  46443  caratheodorylem2  46448  0ome  46450  isomenndlem  46451  hoicvr  46469  hoicvrrex  46477  ovn0lem  46486  ovnsubaddlem1  46491  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem2  46523  hoicoto2  46526  hoi2toco  46528  ovnlecvr2  46531  ovncvr2  46532  ovnsubadd2lem  46566  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  vonioolem1  46601  smfaddlem1  46684  smflimlem2  46693  smflimmpt  46731  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem4  46744  smflimsuplem5  46745  smflimsupmpt  46750  smfliminfmpt  46753  smfsupdmmbllem  46765  finfdm  46767  smfinfdmmbllem  46769  setrec2mpt  48789  aacllem  48895