Theorem fvmpt2 7027

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225   I cid 5577  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fvmptss  7028  fvmpt2d  7029  fvmptd3f  7031  mpteqb  7035  fvmptt  7036  fvmptf  7037  fnmptfvd  7061  ralrnmptw  7114  ralrnmpt  7116  fompt  7138  fmptco  7149  f1mpt  7281  offval2  7717  ofrfval2  7718  fimaproj  8160  mptelixpg  8975  dom2lem  9032  mapxpen  9183  xpmapenlem  9184  cnfcom3clem  9745  tcvalg  9778  rankf  9834  infxpenc2lem2  10060  dfac8clem  10072  acni2  10086  acnlem  10088  fin23lem32  10384  axcc2lem  10476  axcc3  10478  domtriomlem  10482  ac6num  10519  konigthlem  10608  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  seqof  14100  seqof2  14101  rlim2  15532  ello1mpt  15557  o1compt  15623  sumrblem  15747  fsumcvg  15748  summolem2a  15751  fsum  15756  fsumcvg2  15763  fsumadd  15776  isummulc2  15798  fsummulc2  15820  fsumrelem  15843  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  fprod  15977  fprodmul  15996  fproddiv  15997  iserodd  16873  prmrec  16960  prdsbas3  17526  prdsdsval2  17529  invfuc  18022  yonedalem4c  18322  smndex1n0mnd  18925  gsumconst  19952  prdsgsum  19999  gsumdixp  20316  evlslem4  22100  elptr2  23582  ptunimpt  23603  ptcldmpt  23622  ptclsg  23623  txcnp  23628  ptcnplem  23629  cnmpt11  23671  cnmpt1t  23673  cnmptk2  23694  xkocnv  23822  flfcnp2  24015  ustn0  24229  utopsnneiplem  24256  ucnima  24290  iccpnfcnv  24975  ovolctb  25525  ovoliunlem1  25537  ovoliun2  25541  ovolshftlem1  25544  ovolscalem1  25548  voliun  25589  ioombl1lem3  25595  ioombl1lem4  25596  uniioombllem2  25618  mbfeqalem1  25676  mbfpos  25686  mbfposr  25687  mbfposb  25688  mbfsup  25699  mbfinf  25700  mbflim  25703  i1fposd  25742  itg1climres  25749  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2split  25784  itg2mono  25788  itg2cnlem1  25796  isibl2  25801  itgmpt  25818  itgeqa  25849  itggt0  25879  itgcn  25880  limcmpt  25918  dvlipcn  26033  lhop2  26054  dvfsumabs  26063  itgparts  26088  itgsubstlem  26089  itgsubst  26090  elplyd  26241  coeeulem  26263  coeeq2  26281  dvply1  26325  plyremlem  26346  ulmss  26440  ulmdvlem1  26443  mtest  26447  itgulm2  26452  radcnvlem1  26456  pserulm  26465  leibpi  26985  rlimcnp  27008  o1cxp  27018  lgamgulmlem2  27073  lgamgulmlem6  27077  lgamgulm2  27079  sqff1o  27225  lgseisenlem2  27420  dchrvmasumlem1  27539  frgrncvvdeqlem5  30322  ubthlem1  30889  cnlnadjlem5  32090  xppreima2  32661  abfmpunirn  32662  aciunf1lem  32672  suppovss  32690  fpwrelmap  32744  nsgmgc  33440  zringfrac  33582  algextdeglem6  33763  xrmulc1cn  33929  esumpcvgval  34079  esumsup  34090  voliune  34230  eulerpartgbij  34374  signsplypnf  34565  wevgblacfn  35114  iscvm  35264  mclsrcl  35566  f1omptsnlem  37337  matunitlindflem2  37624  itg2addnclem  37678  itggt0cn  37697  ftc1anclem5  37704  pwsgprod  42554  elrfirn2  42707  eq0rabdioph  42787  monotoddzz  42955  aomclem2  43067  refsumcn  45035  refsum2cnlem1  45042  fvmpt2bd  45175  choicefi  45205  axccdom  45227  fvmpt4  45244  fsumsermpt  45594  fmuldfeqlem1  45597  fmuldfeq  45598  climneg  45625  climdivf  45627  mullimc  45631  idlimc  45641  sumnnodd  45645  neglimc  45662  addlimc  45663  0ellimcdiv  45664  climfveqmpt2  45708  climeqmpt  45712  limsupequzmptlem  45743  liminfvalxr  45798  xlimmnfmpt  45858  xlimpnfmpt  45859  cncfmptssg  45886  cncfshift  45889  icccncfext  45902  cncfiooicclem1  45908  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmptdivc  45953  dvnmul  45958  dvnprodlem2  45962  itgsin0pilem1  45965  ibliccsinexp  45966  itgsinexplem1  45969  itgsinexp  45970  ditgeqiooicc  45975  itgsubsticclem  45990  itgioocnicc  45992  stoweidlem2  46017  stoweidlem11  46026  stoweidlem12  46027  stoweidlem16  46031  stoweidlem17  46032  stoweidlem18  46033  stoweidlem19  46034  stoweidlem20  46035  stoweidlem21  46036  stoweidlem22  46037  stoweidlem23  46038  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  stoweidlem36  46051  stoweidlem40  46055  stoweidlem41  46056  stoweidlem42  46057  stoweidlem48  46063  stoweidlem55  46070  stoweidlem59  46074  stoweidlem62  46077  stirlinglem3  46091  stirlinglem8  46096  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  dirkeritg  46117  dirkercncflem2  46119  fourierdlem14  46136  fourierdlem31  46153  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem56  46177  fourierdlem60  46181  fourierdlem61  46182  fourierdlem66  46187  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem77  46198  fourierdlem78  46199  fourierdlem81  46202  fourierdlem83  46204  fourierdlem84  46205  fourierdlem85  46206  fourierdlem87  46208  fourierdlem88  46209  fourierdlem89  46210  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  elaa2lem  46248  etransclem4  46253  etransclem13  46262  etransclem35  46284  etransclem46  46295  etransclem48  46297  sge0revalmpt  46393  sge0fsummpt  46405  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0ltfirpmpt2  46441  sge0fsummptf  46451  nnfoctbdjlem  46470  iundjiun  46475  meaiunlelem  46483  meaiuninclem  46495  meaiuninc3v  46499  omeiunlempt  46535  carageniuncllem2  46537  caratheodorylem2  46542  0ome  46544  isomenndlem  46545  hoicvr  46563  hoicvrrex  46571  ovn0lem  46580  ovnsubaddlem1  46585  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem2  46617  hoicoto2  46620  hoi2toco  46622  ovnlecvr2  46625  ovncvr2  46626  ovnsubadd2lem  46660  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  vonioolem1  46695  smfaddlem1  46778  smflimlem2  46787  smflimmpt  46825  smflimsuplem2  46836  smflimsuplem4  46838  smflimsuplem5  46839  smflimsupmpt  46844  smfliminfmpt  46847  smfsupdmmbllem  46859  finfdm  46861  smfinfdmmbllem  46863  setrec2mpt  49216  aacllem  49320