Theorem fvmpt2 6756

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110   I cid 5424  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fv 6332

This theorem is referenced by:  fvmptss  6757  fvmpt2d  6758  fvmptd3f  6760  mpteqb  6764  fvmptt  6765  fvmptf  6766  fnmptfvd  6788  ralrnmptw  6837  ralrnmpt  6839  fmptco  6868  f1mpt  6997  offval2  7406  ofrfval2  7407  fimaproj  7812  mptelixpg  8482  dom2lem  8532  mapxpen  8667  xpmapenlem  8668  cnfcom3clem  9152  tcvalg  9164  rankf  9207  infxpenc2lem2  9431  dfac8clem  9443  acni2  9457  acnlem  9459  fin23lem32  9755  axcc2lem  9847  axcc3  9849  domtriomlem  9853  ac6num  9890  konigthlem  9979  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  seqof  13423  seqof2  13424  rlim2  14845  ello1mpt  14870  o1compt  14936  sumrblem  15060  fsumcvg  15061  summolem2a  15064  fsum  15069  fsumcvg2  15076  fsumadd  15088  isummulc2  15109  fsummulc2  15131  fsumrelem  15154  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprod  15287  fprodmul  15306  fproddiv  15307  iserodd  16162  prmrec  16248  prdsbas3  16746  prdsdsval2  16749  invfuc  17236  yonedalem4c  17519  smndex1n0mnd  18069  gsumconst  19047  prdsgsum  19094  gsumdixp  19355  evlslem4  20747  elptr2  22179  ptunimpt  22200  ptcldmpt  22219  ptclsg  22220  txcnp  22225  ptcnplem  22226  cnmpt11  22268  cnmpt1t  22270  cnmptk2  22291  xkocnv  22419  flfcnp2  22612  ustn0  22826  utopsnneiplem  22853  ucnima  22887  iccpnfcnv  23549  ovolctb  24094  ovoliunlem1  24106  ovoliun2  24110  ovolshftlem1  24113  ovolscalem1  24117  voliun  24158  ioombl1lem3  24164  ioombl1lem4  24165  uniioombllem2  24187  mbfeqalem1  24245  mbfpos  24255  mbfposr  24256  mbfposb  24257  mbfsup  24268  mbfinf  24269  mbflim  24272  i1fposd  24311  itg1climres  24318  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  itg2split  24353  itg2mono  24357  itg2cnlem1  24365  isibl2  24370  itgmpt  24386  itgeqa  24417  itggt0  24447  itgcn  24448  limcmpt  24486  dvlipcn  24597  lhop2  24618  dvfsumabs  24626  itgparts  24650  itgsubstlem  24651  itgsubst  24652  elplyd  24799  coeeulem  24821  coeeq2  24839  dvply1  24880  plyremlem  24900  ulmss  24992  ulmdvlem1  24995  mtest  24999  itgulm2  25004  radcnvlem1  25008  pserulm  25017  leibpi  25528  rlimcnp  25551  o1cxp  25560  lgamgulmlem2  25615  lgamgulmlem6  25619  lgamgulm2  25621  sqff1o  25767  lgseisenlem2  25960  dchrvmasumlem1  26079  frgrncvvdeqlem5  28088  ubthlem1  28653  cnlnadjlem5  29854  xppreima2  30413  abfmpunirn  30415  aciunf1lem  30425  suppovss  30443  fpwrelmap  30495  xrmulc1cn  31283  esumpcvgval  31447  esumsup  31458  voliune  31598  eulerpartgbij  31740  signsplypnf  31930  iscvm  32619  mclsrcl  32921  f1omptsnlem  34753  matunitlindflem2  35054  itg2addnclem  35108  itggt0cn  35127  ftc1anclem5  35134  elrfirn2  39637  eq0rabdioph  39717  monotoddzz  39884  aomclem2  39999  refsumcn  41659  refsum2cnlem1  41666  fvmpt2bd  41794  fompt  41819  choicefi  41829  axccdom  41853  fvmpt4  41874  fsumsermpt  42221  fmuldfeqlem1  42224  fmuldfeq  42225  climneg  42252  climdivf  42254  mullimc  42258  idlimc  42268  sumnnodd  42272  neglimc  42289  addlimc  42290  0ellimcdiv  42291  climfveqmpt2  42335  climeqmpt  42339  limsupequzmptlem  42370  liminfvalxr  42425  xlimmnfmpt  42485  xlimpnfmpt  42486  cncfmptssg  42513  cncfshift  42516  icccncfext  42529  cncfiooicclem1  42535  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmptdivc  42580  dvnmul  42585  dvnprodlem2  42589  itgsin0pilem1  42592  ibliccsinexp  42593  itgsinexplem1  42596  itgsinexp  42597  ditgeqiooicc  42602  itgsubsticclem  42617  itgioocnicc  42619  stoweidlem2  42644  stoweidlem11  42653  stoweidlem12  42654  stoweidlem16  42658  stoweidlem17  42659  stoweidlem18  42660  stoweidlem19  42661  stoweidlem20  42662  stoweidlem21  42663  stoweidlem22  42664  stoweidlem23  42665  stoweidlem27  42669  stoweidlem31  42673  stoweidlem34  42676  stoweidlem36  42678  stoweidlem40  42682  stoweidlem41  42683  stoweidlem42  42684  stoweidlem48  42690  stoweidlem55  42697  stoweidlem59  42701  stoweidlem62  42704  stirlinglem3  42718  stirlinglem8  42723  stirlinglem14  42729  stirlinglem15  42730  stirlingr  42732  dirkeritg  42744  dirkercncflem2  42746  fourierdlem14  42763  fourierdlem31  42780  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem56  42804  fourierdlem60  42808  fourierdlem61  42809  fourierdlem66  42814  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem77  42825  fourierdlem78  42826  fourierdlem81  42829  fourierdlem83  42831  fourierdlem84  42832  fourierdlem85  42833  fourierdlem87  42835  fourierdlem88  42836  fourierdlem89  42837  fourierdlem91  42839  fourierdlem92  42840  fourierdlem93  42841  fourierdlem95  42843  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  elaa2lem  42875  etransclem4  42880  etransclem13  42889  etransclem35  42911  etransclem46  42922  etransclem48  42924  sge0revalmpt  43017  sge0fsummpt  43029  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0ltfirpmpt2  43065  sge0fsummptf  43075  nnfoctbdjlem  43094  iundjiun  43099  meaiunlelem  43107  meaiuninclem  43119  meaiuninc3v  43123  omeiunlempt  43159  carageniuncllem2  43161  caratheodorylem2  43166  0ome  43168  isomenndlem  43169  hoicvr  43187  hoicvrrex  43195  ovn0lem  43204  ovnsubaddlem1  43209  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem2  43241  hoicoto2  43244  hoi2toco  43246  ovnlecvr2  43249  ovncvr2  43250  ovnsubadd2lem  43284  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  vonioolem1  43319  smfaddlem1  43396  smflimlem2  43405  smflimmpt  43441  smfsupmpt  43446  smfinfmpt  43450  smflimsuplem2  43452  smflimsuplem4  43454  smflimsuplem5  43455  smflimsupmpt  43460  smfliminfmpt  43463  aacllem  45329