Theorem fvmpt2 6946

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5174   I cid 5513  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmptss  6947  fvmpt2d  6948  fvmptd3f  6950  mpteqb  6954  fvmptt  6955  fvmptf  6956  fnmptfvd  6980  ralrnmptw  7033  ralrnmpt  7035  fompt  7057  fmptco  7068  f1mpt  7201  offval2  7636  ofrfval2  7637  fimaproj  8071  mptelixpg  8865  dom2lem  8921  mapxpen  9063  xpmapenlem  9064  cnfcom3clem  9602  tcvalg  9633  rankf  9694  infxpenc2lem2  9918  dfac8clem  9930  acni2  9944  acnlem  9946  fin23lem32  10242  axcc2lem  10334  axcc3  10336  domtriomlem  10340  ac6num  10377  konigthlem  10466  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem5  12881  seqof  13968  seqof2  13969  rlim2  15405  ello1mpt  15430  o1compt  15496  sumrblem  15620  fsumcvg  15621  summolem2a  15624  fsum  15629  fsumcvg2  15636  fsumadd  15649  isummulc2  15671  fsummulc2  15693  fsumrelem  15716  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  zprod  15846  fprod  15850  fprodmul  15869  fproddiv  15870  iserodd  16749  prmrec  16836  prdsbas3  17387  prdsdsval2  17390  invfuc  17886  yonedalem4c  18185  smndex1n0mnd  18822  gsumconst  19848  prdsgsum  19895  gsumdixp  20239  evlslem4  22012  elptr2  23490  ptunimpt  23511  ptcldmpt  23530  ptclsg  23531  txcnp  23536  ptcnplem  23537  cnmpt11  23579  cnmpt1t  23581  cnmptk2  23602  xkocnv  23730  flfcnp2  23923  ustn0  24137  utopsnneiplem  24163  ucnima  24196  iccpnfcnv  24870  ovolctb  25419  ovoliunlem1  25431  ovoliun2  25435  ovolshftlem1  25438  ovolscalem1  25442  voliun  25483  ioombl1lem3  25489  ioombl1lem4  25490  uniioombllem2  25512  mbfeqalem1  25570  mbfpos  25580  mbfposr  25581  mbfposb  25582  mbfsup  25593  mbfinf  25594  mbflim  25597  i1fposd  25636  itg1climres  25643  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  itg2split  25678  itg2mono  25682  itg2cnlem1  25690  isibl2  25695  itgmpt  25712  itgeqa  25743  itggt0  25773  itgcn  25774  limcmpt  25812  dvlipcn  25927  lhop2  25948  dvfsumabs  25957  itgparts  25982  itgsubstlem  25983  itgsubst  25984  elplyd  26135  coeeulem  26157  coeeq2  26175  dvply1  26219  plyremlem  26240  ulmss  26334  ulmdvlem1  26337  mtest  26341  itgulm2  26346  radcnvlem1  26350  pserulm  26359  leibpi  26880  rlimcnp  26903  o1cxp  26913  lgamgulmlem2  26968  lgamgulmlem6  26972  lgamgulm2  26974  sqff1o  27120  lgseisenlem2  27315  dchrvmasumlem1  27434  frgrncvvdeqlem5  30285  ubthlem1  30852  cnlnadjlem5  32053  xppreima2  32635  abfmpunirn  32636  aciunf1lem  32646  suppovss  32666  fpwrelmap  32720  nsgmgc  33384  zringfrac  33526  extdgfialglem2  33727  algextdeglem6  33756  xrmulc1cn  33964  esumpcvgval  34112  esumsup  34123  voliune  34263  eulerpartgbij  34406  signsplypnf  34584  wevgblacfn  35174  iscvm  35324  mclsrcl  35626  f1omptsnlem  37401  matunitlindflem2  37677  itg2addnclem  37731  itggt0cn  37750  ftc1anclem5  37757  pwsgprod  42662  elrfirn2  42813  eq0rabdioph  42893  monotoddzz  43060  aomclem2  43172  refsumcn  45151  refsum2cnlem1  45158  fvmpt2bd  45291  choicefi  45321  axccdom  45343  fvmpt4  45359  fsumsermpt  45703  fmuldfeqlem1  45706  fmuldfeq  45707  climneg  45734  climdivf  45736  mullimc  45740  idlimc  45750  sumnnodd  45754  neglimc  45769  addlimc  45770  0ellimcdiv  45771  climfveqmpt2  45815  climeqmpt  45819  limsupequzmptlem  45850  liminfvalxr  45905  xlimmnfmpt  45965  xlimpnfmpt  45966  cncfmptssg  45993  cncfshift  45996  icccncfext  46009  cncfiooicclem1  46015  fprodsubrecnncnvlem  46029  fprodaddrecnncnvlem  46031  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnmptdivc  46060  dvnmul  46065  dvnprodlem2  46069  itgsin0pilem1  46072  ibliccsinexp  46073  itgsinexplem1  46076  itgsinexp  46077  ditgeqiooicc  46082  itgsubsticclem  46097  itgioocnicc  46099  stoweidlem2  46124  stoweidlem11  46133  stoweidlem12  46134  stoweidlem16  46138  stoweidlem17  46139  stoweidlem18  46140  stoweidlem19  46141  stoweidlem20  46142  stoweidlem21  46143  stoweidlem22  46144  stoweidlem23  46145  stoweidlem27  46149  stoweidlem31  46153  stoweidlem34  46156  stoweidlem36  46158  stoweidlem40  46162  stoweidlem41  46163  stoweidlem42  46164  stoweidlem48  46170  stoweidlem55  46177  stoweidlem59  46181  stoweidlem62  46184  stirlinglem3  46198  stirlinglem8  46203  stirlinglem14  46209  stirlinglem15  46210  stirlingr  46212  dirkeritg  46224  dirkercncflem2  46226  fourierdlem14  46243  fourierdlem31  46260  fourierdlem41  46270  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem51  46279  fourierdlem56  46284  fourierdlem60  46288  fourierdlem61  46289  fourierdlem66  46294  fourierdlem70  46298  fourierdlem71  46299  fourierdlem73  46301  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem77  46305  fourierdlem78  46306  fourierdlem81  46309  fourierdlem83  46311  fourierdlem84  46312  fourierdlem85  46313  fourierdlem87  46315  fourierdlem88  46316  fourierdlem89  46317  fourierdlem91  46319  fourierdlem92  46320  fourierdlem93  46321  fourierdlem95  46323  fourierdlem97  46325  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  sqwvfoura  46350  sqwvfourb  46351  fouriersw  46353  elaa2lem  46355  etransclem4  46360  etransclem13  46369  etransclem35  46391  etransclem46  46402  etransclem48  46404  sge0revalmpt  46500  sge0fsummpt  46512  sge0iunmptlemfi  46535  sge0iunmptlemre  46537  sge0ltfirpmpt2  46548  sge0fsummptf  46558  nnfoctbdjlem  46577  iundjiun  46582  meaiunlelem  46590  meaiuninclem  46602  meaiuninc3v  46606  omeiunlempt  46642  carageniuncllem2  46644  caratheodorylem2  46649  0ome  46651  isomenndlem  46652  hoicvr  46670  hoicvrrex  46678  ovn0lem  46687  ovnsubaddlem1  46692  hoidmvlelem2  46718  hoidmvlelem3  46719  ovnhoilem2  46724  hoicoto2  46727  hoi2toco  46729  ovnlecvr2  46732  ovncvr2  46733  ovnsubadd2lem  46767  ovolval5lem2  46775  ovnovollem1  46778  ovnovollem2  46779  vonioolem1  46802  smfaddlem1  46885  smflimlem2  46894  smflimmpt  46932  smflimsuplem2  46943  smflimsuplem4  46945  smflimsuplem5  46946  smflimsupmpt  46951  smfliminfmpt  46954  smfsupdmmbllem  46966  finfdm  46968  smfinfdmmbllem  46970  setrec2mpt  49822  aacllem  49926