Theorem fvmpt2 6982

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191   I cid 5535  ‘cfv 6514

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fvmptss  6983  fvmpt2d  6984  fvmptd3f  6986  mpteqb  6990  fvmptt  6991  fvmptf  6992  fnmptfvd  7016  ralrnmptw  7069  ralrnmpt  7071  fompt  7093  fmptco  7104  f1mpt  7239  offval2  7676  ofrfval2  7677  fimaproj  8117  mptelixpg  8911  dom2lem  8966  mapxpen  9113  xpmapenlem  9114  cnfcom3clem  9665  tcvalg  9698  rankf  9754  infxpenc2lem2  9980  dfac8clem  9992  acni2  10006  acnlem  10008  fin23lem32  10304  axcc2lem  10396  axcc3  10398  domtriomlem  10402  ac6num  10439  konigthlem  10528  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  seqof  14031  seqof2  14032  rlim2  15469  ello1mpt  15494  o1compt  15560  sumrblem  15684  fsumcvg  15685  summolem2a  15688  fsum  15693  fsumcvg2  15700  fsumadd  15713  isummulc2  15735  fsummulc2  15757  fsumrelem  15780  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  fprod  15914  fprodmul  15933  fproddiv  15934  iserodd  16813  prmrec  16900  prdsbas3  17451  prdsdsval2  17454  invfuc  17946  yonedalem4c  18245  smndex1n0mnd  18846  gsumconst  19871  prdsgsum  19918  gsumdixp  20235  evlslem4  21990  elptr2  23468  ptunimpt  23489  ptcldmpt  23508  ptclsg  23509  txcnp  23514  ptcnplem  23515  cnmpt11  23557  cnmpt1t  23559  cnmptk2  23580  xkocnv  23708  flfcnp2  23901  ustn0  24115  utopsnneiplem  24142  ucnima  24175  iccpnfcnv  24849  ovolctb  25398  ovoliunlem1  25410  ovoliun2  25414  ovolshftlem1  25417  ovolscalem1  25421  voliun  25462  ioombl1lem3  25468  ioombl1lem4  25469  uniioombllem2  25491  mbfeqalem1  25549  mbfpos  25559  mbfposr  25560  mbfposb  25561  mbfsup  25572  mbfinf  25573  mbflim  25576  i1fposd  25615  itg1climres  25622  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2split  25657  itg2mono  25661  itg2cnlem1  25669  isibl2  25674  itgmpt  25691  itgeqa  25722  itggt0  25752  itgcn  25753  limcmpt  25791  dvlipcn  25906  lhop2  25927  dvfsumabs  25936  itgparts  25961  itgsubstlem  25962  itgsubst  25963  elplyd  26114  coeeulem  26136  coeeq2  26154  dvply1  26198  plyremlem  26219  ulmss  26313  ulmdvlem1  26316  mtest  26320  itgulm2  26325  radcnvlem1  26329  pserulm  26338  leibpi  26859  rlimcnp  26882  o1cxp  26892  lgamgulmlem2  26947  lgamgulmlem6  26951  lgamgulm2  26953  sqff1o  27099  lgseisenlem2  27294  dchrvmasumlem1  27413  frgrncvvdeqlem5  30239  ubthlem1  30806  cnlnadjlem5  32007  xppreima2  32582  abfmpunirn  32583  aciunf1lem  32593  suppovss  32611  fpwrelmap  32663  nsgmgc  33390  zringfrac  33532  algextdeglem6  33719  xrmulc1cn  33927  esumpcvgval  34075  esumsup  34086  voliune  34226  eulerpartgbij  34370  signsplypnf  34548  wevgblacfn  35103  iscvm  35253  mclsrcl  35555  f1omptsnlem  37331  matunitlindflem2  37618  itg2addnclem  37672  itggt0cn  37691  ftc1anclem5  37698  pwsgprod  42539  elrfirn2  42691  eq0rabdioph  42771  monotoddzz  42939  aomclem2  43051  refsumcn  45031  refsum2cnlem1  45038  fvmpt2bd  45171  choicefi  45201  axccdom  45223  fvmpt4  45239  fsumsermpt  45584  fmuldfeqlem1  45587  fmuldfeq  45588  climneg  45615  climdivf  45617  mullimc  45621  idlimc  45631  sumnnodd  45635  neglimc  45652  addlimc  45653  0ellimcdiv  45654  climfveqmpt2  45698  climeqmpt  45702  limsupequzmptlem  45733  liminfvalxr  45788  xlimmnfmpt  45848  xlimpnfmpt  45849  cncfmptssg  45876  cncfshift  45879  icccncfext  45892  cncfiooicclem1  45898  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmptdivc  45943  dvnmul  45948  dvnprodlem2  45952  itgsin0pilem1  45955  ibliccsinexp  45956  itgsinexplem1  45959  itgsinexp  45960  ditgeqiooicc  45965  itgsubsticclem  45980  itgioocnicc  45982  stoweidlem2  46007  stoweidlem11  46016  stoweidlem12  46017  stoweidlem16  46021  stoweidlem17  46022  stoweidlem18  46023  stoweidlem19  46024  stoweidlem20  46025  stoweidlem21  46026  stoweidlem22  46027  stoweidlem23  46028  stoweidlem27  46032  stoweidlem31  46036  stoweidlem34  46039  stoweidlem36  46041  stoweidlem40  46045  stoweidlem41  46046  stoweidlem42  46047  stoweidlem48  46053  stoweidlem55  46060  stoweidlem59  46064  stoweidlem62  46067  stirlinglem3  46081  stirlinglem8  46086  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  dirkeritg  46107  dirkercncflem2  46109  fourierdlem14  46126  fourierdlem31  46143  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem56  46167  fourierdlem60  46171  fourierdlem61  46172  fourierdlem66  46177  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem77  46188  fourierdlem78  46189  fourierdlem81  46192  fourierdlem83  46194  fourierdlem84  46195  fourierdlem85  46196  fourierdlem87  46198  fourierdlem88  46199  fourierdlem89  46200  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  elaa2lem  46238  etransclem4  46243  etransclem13  46252  etransclem35  46274  etransclem46  46285  etransclem48  46287  sge0revalmpt  46383  sge0fsummpt  46395  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0ltfirpmpt2  46431  sge0fsummptf  46441  nnfoctbdjlem  46460  iundjiun  46465  meaiunlelem  46473  meaiuninclem  46485  meaiuninc3v  46489  omeiunlempt  46525  carageniuncllem2  46527  caratheodorylem2  46532  0ome  46534  isomenndlem  46535  hoicvr  46553  hoicvrrex  46561  ovn0lem  46570  ovnsubaddlem1  46575  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem2  46607  hoicoto2  46610  hoi2toco  46612  ovnlecvr2  46615  ovncvr2  46616  ovnsubadd2lem  46650  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  vonioolem1  46685  smfaddlem1  46768  smflimlem2  46777  smflimmpt  46815  smflimsuplem2  46826  smflimsuplem4  46828  smflimsuplem5  46829  smflimsupmpt  46834  smfliminfmpt  46837  smfsupdmmbllem  46849  finfdm  46851  smfinfdmmbllem  46853  setrec2mpt  49690  aacllem  49794