Theorem fvmpt2 7026

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230   I cid 5581  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  fvmptss  7027  fvmpt2d  7028  fvmptd3f  7030  mpteqb  7034  fvmptt  7035  fvmptf  7036  fnmptfvd  7060  ralrnmptw  7113  ralrnmpt  7115  fompt  7137  fmptco  7148  f1mpt  7280  offval2  7716  ofrfval2  7717  fimaproj  8158  mptelixpg  8973  dom2lem  9030  mapxpen  9181  xpmapenlem  9182  cnfcom3clem  9742  tcvalg  9775  rankf  9831  infxpenc2lem2  10057  dfac8clem  10069  acni2  10083  acnlem  10085  fin23lem32  10381  axcc2lem  10473  axcc3  10475  domtriomlem  10479  ac6num  10516  konigthlem  10605  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  seqof  14096  seqof2  14097  rlim2  15528  ello1mpt  15553  o1compt  15619  sumrblem  15743  fsumcvg  15744  summolem2a  15747  fsum  15752  fsumcvg2  15759  fsumadd  15772  isummulc2  15794  fsummulc2  15816  fsumrelem  15839  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  fprod  15973  fprodmul  15992  fproddiv  15993  iserodd  16868  prmrec  16955  prdsbas3  17527  prdsdsval2  17530  invfuc  18030  yonedalem4c  18333  smndex1n0mnd  18937  gsumconst  19966  prdsgsum  20013  gsumdixp  20332  evlslem4  22117  elptr2  23597  ptunimpt  23618  ptcldmpt  23637  ptclsg  23638  txcnp  23643  ptcnplem  23644  cnmpt11  23686  cnmpt1t  23688  cnmptk2  23709  xkocnv  23837  flfcnp2  24030  ustn0  24244  utopsnneiplem  24271  ucnima  24305  iccpnfcnv  24988  ovolctb  25538  ovoliunlem1  25550  ovoliun2  25554  ovolshftlem1  25557  ovolscalem1  25561  voliun  25602  ioombl1lem3  25608  ioombl1lem4  25609  uniioombllem2  25631  mbfeqalem1  25689  mbfpos  25699  mbfposr  25700  mbfposb  25701  mbfsup  25712  mbfinf  25713  mbflim  25716  i1fposd  25756  itg1climres  25763  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2split  25798  itg2mono  25802  itg2cnlem1  25810  isibl2  25815  itgmpt  25832  itgeqa  25863  itggt0  25893  itgcn  25894  limcmpt  25932  dvlipcn  26047  lhop2  26068  dvfsumabs  26077  itgparts  26102  itgsubstlem  26103  itgsubst  26104  elplyd  26255  coeeulem  26277  coeeq2  26295  dvply1  26339  plyremlem  26360  ulmss  26454  ulmdvlem1  26457  mtest  26461  itgulm2  26466  radcnvlem1  26470  pserulm  26479  leibpi  26999  rlimcnp  27022  o1cxp  27032  lgamgulmlem2  27087  lgamgulmlem6  27091  lgamgulm2  27093  sqff1o  27239  lgseisenlem2  27434  dchrvmasumlem1  27553  frgrncvvdeqlem5  30331  ubthlem1  30898  cnlnadjlem5  32099  xppreima2  32667  abfmpunirn  32668  aciunf1lem  32678  suppovss  32695  fpwrelmap  32750  nsgmgc  33419  zringfrac  33561  algextdeglem6  33727  xrmulc1cn  33890  esumpcvgval  34058  esumsup  34069  voliune  34209  eulerpartgbij  34353  signsplypnf  34543  wevgblacfn  35092  iscvm  35243  mclsrcl  35545  f1omptsnlem  37318  matunitlindflem2  37603  itg2addnclem  37657  itggt0cn  37676  ftc1anclem5  37683  pwsgprod  42530  elrfirn2  42683  eq0rabdioph  42763  monotoddzz  42931  aomclem2  43043  refsumcn  44967  refsum2cnlem1  44974  fvmpt2bd  45112  choicefi  45142  axccdom  45164  fvmpt4  45181  fsumsermpt  45534  fmuldfeqlem1  45537  fmuldfeq  45538  climneg  45565  climdivf  45567  mullimc  45571  idlimc  45581  sumnnodd  45585  neglimc  45602  addlimc  45603  0ellimcdiv  45604  climfveqmpt2  45648  climeqmpt  45652  limsupequzmptlem  45683  liminfvalxr  45738  xlimmnfmpt  45798  xlimpnfmpt  45799  cncfmptssg  45826  cncfshift  45829  icccncfext  45842  cncfiooicclem1  45848  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmptdivc  45893  dvnmul  45898  dvnprodlem2  45902  itgsin0pilem1  45905  ibliccsinexp  45906  itgsinexplem1  45909  itgsinexp  45910  ditgeqiooicc  45915  itgsubsticclem  45930  itgioocnicc  45932  stoweidlem2  45957  stoweidlem11  45966  stoweidlem12  45967  stoweidlem16  45971  stoweidlem17  45972  stoweidlem18  45973  stoweidlem19  45974  stoweidlem20  45975  stoweidlem21  45976  stoweidlem22  45977  stoweidlem23  45978  stoweidlem27  45982  stoweidlem31  45986  stoweidlem34  45989  stoweidlem36  45991  stoweidlem40  45995  stoweidlem41  45996  stoweidlem42  45997  stoweidlem48  46003  stoweidlem55  46010  stoweidlem59  46014  stoweidlem62  46017  stirlinglem3  46031  stirlinglem8  46036  stirlinglem14  46042  stirlinglem15  46043  stirlingr  46045  dirkeritg  46057  dirkercncflem2  46059  fourierdlem14  46076  fourierdlem31  46093  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem56  46117  fourierdlem60  46121  fourierdlem61  46122  fourierdlem66  46127  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem77  46138  fourierdlem78  46139  fourierdlem81  46142  fourierdlem83  46144  fourierdlem84  46145  fourierdlem85  46146  fourierdlem87  46148  fourierdlem88  46149  fourierdlem89  46150  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  elaa2lem  46188  etransclem4  46193  etransclem13  46202  etransclem35  46224  etransclem46  46235  etransclem48  46237  sge0revalmpt  46333  sge0fsummpt  46345  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0ltfirpmpt2  46381  sge0fsummptf  46391  nnfoctbdjlem  46410  iundjiun  46415  meaiunlelem  46423  meaiuninclem  46435  meaiuninc3v  46439  omeiunlempt  46475  carageniuncllem2  46477  caratheodorylem2  46482  0ome  46484  isomenndlem  46485  hoicvr  46503  hoicvrrex  46511  ovn0lem  46520  ovnsubaddlem1  46525  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem2  46557  hoicoto2  46560  hoi2toco  46562  ovnlecvr2  46565  ovncvr2  46566  ovnsubadd2lem  46600  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  vonioolem1  46635  smfaddlem1  46718  smflimlem2  46727  smflimmpt  46765  smflimsuplem2  46776  smflimsuplem4  46778  smflimsuplem5  46779  smflimsupmpt  46784  smfliminfmpt  46787  smfsupdmmbllem  46799  finfdm  46801  smfinfdmmbllem  46803  setrec2mpt  48927  aacllem  49031