Theorem fvmpt2 6782

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ↦ cmpt 5149   I cid 5462  ‘cfv 6358

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fv 6366

This theorem is referenced by:  fvmptss  6783  fvmpt2d  6784  fvmptd3f  6786  mpteqb  6790  fvmptt  6791  fvmptf  6792  fnmptfvd  6814  ralrnmptw  6863  ralrnmpt  6865  fmptco  6894  f1mpt  7022  offval2  7429  ofrfval2  7430  fimaproj  7832  mptelixpg  8502  dom2lem  8552  mapxpen  8686  xpmapenlem  8687  cnfcom3clem  9171  tcvalg  9183  rankf  9226  infxpenc2lem2  9449  dfac8clem  9461  acni2  9475  acnlem  9477  fin23lem32  9769  axcc2lem  9861  axcc3  9863  domtriomlem  9867  ac6num  9904  konigthlem  9993  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  seqof  13430  seqof2  13431  rlim2  14856  ello1mpt  14881  o1compt  14947  sumrblem  15071  fsumcvg  15072  summolem2a  15075  fsum  15080  fsumcvg2  15087  fsumadd  15099  isummulc2  15120  fsummulc2  15142  fsumrelem  15165  prodrblem  15286  fprodcvg  15287  prodmolem2a  15291  zprod  15294  fprod  15298  fprodmul  15317  fproddiv  15318  iserodd  16175  prmrec  16261  prdsbas3  16757  prdsdsval2  16760  invfuc  17247  yonedalem4c  17530  smndex1n0mnd  18080  gsumconst  19057  prdsgsum  19104  gsumdixp  19362  evlslem4  20291  elptr2  22185  ptunimpt  22206  ptcldmpt  22225  ptclsg  22226  txcnp  22231  ptcnplem  22232  cnmpt11  22274  cnmpt1t  22276  cnmptk2  22297  xkocnv  22425  flfcnp2  22618  ustn0  22832  utopsnneiplem  22859  ucnima  22893  iccpnfcnv  23551  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  24445  itgcn  24446  limcmpt  24484  dvlipcn  24594  lhop2  24615  dvfsumabs  24623  itgparts  24647  itgsubstlem  24648  itgsubst  24649  elplyd  24795  coeeulem  24817  coeeq2  24835  dvply1  24876  plyremlem  24896  ulmss  24988  ulmdvlem1  24991  mtest  24995  itgulm2  25000  radcnvlem1  25004  pserulm  25013  leibpi  25523  rlimcnp  25546  o1cxp  25555  lgamgulmlem2  25610  lgamgulmlem6  25614  lgamgulm2  25616  sqff1o  25762  lgseisenlem2  25955  dchrvmasumlem1  26074  frgrncvvdeqlem5  28085  ubthlem1  28650  cnlnadjlem5  29851  xppreima2  30398  abfmpunirn  30400  aciunf1lem  30410  suppovss  30429  fpwrelmap  30472  xrmulc1cn  31177  esumpcvgval  31341  esumsup  31352  voliune  31492  eulerpartgbij  31634  signsplypnf  31824  iscvm  32510  mclsrcl  32812  f1omptsnlem  34621  matunitlindflem2  34893  itg2addnclem  34947  itggt0cn  34968  ftc1anclem5  34975  elrfirn2  39299  eq0rabdioph  39379  monotoddzz  39546  aomclem2  39661  refsumcn  41293  refsum2cnlem1  41300  fvmpt2bd  41432  fompt  41459  choicefi  41469  axccdom  41493  fvmpt4  41514  fsumsermpt  41866  fmuldfeqlem1  41869  fmuldfeq  41870  climneg  41897  climdivf  41899  mullimc  41903  idlimc  41913  sumnnodd  41917  neglimc  41934  addlimc  41935  0ellimcdiv  41936  climfveqmpt2  41980  climeqmpt  41984  limsupequzmptlem  42015  liminfvalxr  42070  xlimmnfmpt  42130  xlimpnfmpt  42131  cncfmptssg  42159  cncfshift  42163  icccncfext  42176  cncfiooicclem1  42182  fprodsubrecnncnvlem  42197  fprodaddrecnncnvlem  42199  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnmptdivc  42229  dvnmul  42234  dvnprodlem2  42238  itgsin0pilem1  42241  ibliccsinexp  42242  itgsinexplem1  42245  itgsinexp  42246  ditgeqiooicc  42251  itgsubsticclem  42266  itgioocnicc  42268  stoweidlem2  42294  stoweidlem11  42303  stoweidlem12  42304  stoweidlem16  42308  stoweidlem17  42309  stoweidlem18  42310  stoweidlem19  42311  stoweidlem20  42312  stoweidlem21  42313  stoweidlem22  42314  stoweidlem23  42315  stoweidlem27  42319  stoweidlem31  42323  stoweidlem34  42326  stoweidlem36  42328  stoweidlem40  42332  stoweidlem41  42333  stoweidlem42  42334  stoweidlem48  42340  stoweidlem55  42347  stoweidlem59  42351  stoweidlem62  42354  stirlinglem3  42368  stirlinglem8  42373  stirlinglem14  42379  stirlinglem15  42380  stirlingr  42382  dirkeritg  42394  dirkercncflem2  42396  fourierdlem14  42413  fourierdlem31  42430  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem51  42449  fourierdlem56  42454  fourierdlem60  42458  fourierdlem61  42459  fourierdlem66  42464  fourierdlem70  42468  fourierdlem71  42469  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem77  42475  fourierdlem78  42476  fourierdlem81  42479  fourierdlem83  42481  fourierdlem84  42482  fourierdlem85  42483  fourierdlem87  42485  fourierdlem88  42486  fourierdlem89  42487  fourierdlem91  42489  fourierdlem92  42490  fourierdlem93  42491  fourierdlem95  42493  fourierdlem97  42495  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  elaa2lem  42525  etransclem4  42530  etransclem13  42539  etransclem35  42561  etransclem46  42572  etransclem48  42574  sge0revalmpt  42667  sge0fsummpt  42679  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0ltfirpmpt2  42715  sge0fsummptf  42725  nnfoctbdjlem  42744  iundjiun  42749  meaiunlelem  42757  meaiuninclem  42769  meaiuninc3v  42773  omeiunlempt  42809  carageniuncllem2  42811  caratheodorylem2  42816  0ome  42818  isomenndlem  42819  hoicvr  42837  hoicvrrex  42845  ovn0lem  42854  ovnsubaddlem1  42859  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem2  42891  hoicoto2  42894  hoi2toco  42896  ovnlecvr2  42899  ovncvr2  42900  ovnsubadd2lem  42934  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  vonioolem1  42969  smfaddlem1  43046  smflimlem2  43055  smflimmpt  43091  smfsupmpt  43096  smfinfmpt  43100  smflimsuplem2  43102  smflimsuplem4  43104  smflimsuplem5  43105  smflimsupmpt  43110  smfliminfmpt  43113  aacllem  44909