Theorem fvmpt2 6940

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172   I cid 5510  ‘cfv 6481

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  fvmptss  6941  fvmpt2d  6942  fvmptd3f  6944  mpteqb  6948  fvmptt  6949  fvmptf  6950  fnmptfvd  6974  ralrnmptw  7027  ralrnmpt  7029  fompt  7051  fmptco  7062  f1mpt  7195  offval2  7630  ofrfval2  7631  fimaproj  8065  mptelixpg  8859  dom2lem  8914  mapxpen  9056  xpmapenlem  9057  cnfcom3clem  9595  tcvalg  9628  rankf  9684  infxpenc2lem2  9908  dfac8clem  9920  acni2  9934  acnlem  9936  fin23lem32  10232  axcc2lem  10324  axcc3  10326  domtriomlem  10330  ac6num  10367  konigthlem  10456  rpnnen1lem1  12873  rpnnen1lem3  12874  rpnnen1lem5  12876  seqof  13963  seqof2  13964  rlim2  15400  ello1mpt  15425  o1compt  15491  sumrblem  15615  fsumcvg  15616  summolem2a  15619  fsum  15624  fsumcvg2  15631  fsumadd  15644  isummulc2  15666  fsummulc2  15688  fsumrelem  15711  prodrblem  15833  fprodcvg  15834  prodmolem2a  15838  zprod  15841  fprod  15845  fprodmul  15864  fproddiv  15865  iserodd  16744  prmrec  16831  prdsbas3  17382  prdsdsval2  17385  invfuc  17881  yonedalem4c  18180  smndex1n0mnd  18817  gsumconst  19844  prdsgsum  19891  gsumdixp  20235  evlslem4  22009  elptr2  23487  ptunimpt  23508  ptcldmpt  23527  ptclsg  23528  txcnp  23533  ptcnplem  23534  cnmpt11  23576  cnmpt1t  23578  cnmptk2  23599  xkocnv  23727  flfcnp2  23920  ustn0  24134  utopsnneiplem  24160  ucnima  24193  iccpnfcnv  24867  ovolctb  25416  ovoliunlem1  25428  ovoliun2  25432  ovolshftlem1  25435  ovolscalem1  25439  voliun  25480  ioombl1lem3  25486  ioombl1lem4  25487  uniioombllem2  25509  mbfeqalem1  25567  mbfpos  25577  mbfposr  25578  mbfposb  25579  mbfsup  25590  mbfinf  25591  mbflim  25594  i1fposd  25633  itg1climres  25640  mbfi1fseqlem4  25644  mbfi1fseqlem5  25645  mbfi1fseqlem6  25646  itg2split  25675  itg2mono  25679  itg2cnlem1  25687  isibl2  25692  itgmpt  25709  itgeqa  25740  itggt0  25770  itgcn  25771  limcmpt  25809  dvlipcn  25924  lhop2  25945  dvfsumabs  25954  itgparts  25979  itgsubstlem  25980  itgsubst  25981  elplyd  26132  coeeulem  26154  coeeq2  26172  dvply1  26216  plyremlem  26237  ulmss  26331  ulmdvlem1  26334  mtest  26338  itgulm2  26343  radcnvlem1  26347  pserulm  26356  leibpi  26877  rlimcnp  26900  o1cxp  26910  lgamgulmlem2  26965  lgamgulmlem6  26969  lgamgulm2  26971  sqff1o  27117  lgseisenlem2  27312  dchrvmasumlem1  27431  frgrncvvdeqlem5  30278  ubthlem1  30845  cnlnadjlem5  32046  xppreima2  32628  abfmpunirn  32629  aciunf1lem  32639  suppovss  32657  fpwrelmap  32711  nsgmgc  33372  zringfrac  33514  extdgfialglem2  33701  algextdeglem6  33730  xrmulc1cn  33938  esumpcvgval  34086  esumsup  34097  voliune  34237  eulerpartgbij  34380  signsplypnf  34558  wevgblacfn  35141  iscvm  35291  mclsrcl  35593  f1omptsnlem  37369  matunitlindflem2  37656  itg2addnclem  37710  itggt0cn  37729  ftc1anclem5  37736  pwsgprod  42576  elrfirn2  42728  eq0rabdioph  42808  monotoddzz  42975  aomclem2  43087  refsumcn  45066  refsum2cnlem1  45073  fvmpt2bd  45206  choicefi  45236  axccdom  45258  fvmpt4  45274  fsumsermpt  45618  fmuldfeqlem1  45621  fmuldfeq  45622  climneg  45649  climdivf  45651  mullimc  45655  idlimc  45665  sumnnodd  45669  neglimc  45684  addlimc  45685  0ellimcdiv  45686  climfveqmpt2  45730  climeqmpt  45734  limsupequzmptlem  45765  liminfvalxr  45820  xlimmnfmpt  45880  xlimpnfmpt  45881  cncfmptssg  45908  cncfshift  45911  icccncfext  45924  cncfiooicclem1  45930  fprodsubrecnncnvlem  45944  fprodaddrecnncnvlem  45946  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnmptdivc  45975  dvnmul  45980  dvnprodlem2  45984  itgsin0pilem1  45987  ibliccsinexp  45988  itgsinexplem1  45991  itgsinexp  45992  ditgeqiooicc  45997  itgsubsticclem  46012  itgioocnicc  46014  stoweidlem2  46039  stoweidlem11  46048  stoweidlem12  46049  stoweidlem16  46053  stoweidlem17  46054  stoweidlem18  46055  stoweidlem19  46056  stoweidlem20  46057  stoweidlem21  46058  stoweidlem22  46059  stoweidlem23  46060  stoweidlem27  46064  stoweidlem31  46068  stoweidlem34  46071  stoweidlem36  46073  stoweidlem40  46077  stoweidlem41  46078  stoweidlem42  46079  stoweidlem48  46085  stoweidlem55  46092  stoweidlem59  46096  stoweidlem62  46099  stirlinglem3  46113  stirlinglem8  46118  stirlinglem14  46124  stirlinglem15  46125  stirlingr  46127  dirkeritg  46139  dirkercncflem2  46141  fourierdlem14  46158  fourierdlem31  46175  fourierdlem41  46185  fourierdlem48  46191  fourierdlem49  46192  fourierdlem50  46193  fourierdlem51  46194  fourierdlem56  46199  fourierdlem60  46203  fourierdlem61  46204  fourierdlem66  46209  fourierdlem70  46213  fourierdlem71  46214  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem77  46220  fourierdlem78  46221  fourierdlem81  46224  fourierdlem83  46226  fourierdlem84  46227  fourierdlem85  46228  fourierdlem87  46230  fourierdlem88  46231  fourierdlem89  46232  fourierdlem91  46234  fourierdlem92  46235  fourierdlem93  46236  fourierdlem95  46238  fourierdlem97  46240  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  sqwvfoura  46265  sqwvfourb  46266  fouriersw  46268  elaa2lem  46270  etransclem4  46275  etransclem13  46284  etransclem35  46306  etransclem46  46317  etransclem48  46319  sge0revalmpt  46415  sge0fsummpt  46427  sge0iunmptlemfi  46450  sge0iunmptlemre  46452  sge0ltfirpmpt2  46463  sge0fsummptf  46473  nnfoctbdjlem  46492  iundjiun  46497  meaiunlelem  46505  meaiuninclem  46517  meaiuninc3v  46521  omeiunlempt  46557  carageniuncllem2  46559  caratheodorylem2  46564  0ome  46566  isomenndlem  46567  hoicvr  46585  hoicvrrex  46593  ovn0lem  46602  ovnsubaddlem1  46607  hoidmvlelem2  46633  hoidmvlelem3  46634  ovnhoilem2  46639  hoicoto2  46642  hoi2toco  46644  ovnlecvr2  46647  ovncvr2  46648  ovnsubadd2lem  46682  ovolval5lem2  46690  ovnovollem1  46693  ovnovollem2  46694  vonioolem1  46717  smfaddlem1  46800  smflimlem2  46809  smflimmpt  46847  smflimsuplem2  46858  smflimsuplem4  46860  smflimsuplem5  46861  smflimsupmpt  46866  smfliminfmpt  46869  smfsupdmmbllem  46881  finfdm  46883  smfinfdmmbllem  46885  setrec2mpt  49728  aacllem  49832