Theorem fvmpt2 6952

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179   I cid 5518  ‘cfv 6492

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptss  6953  fvmpt2d  6954  fvmptd3f  6956  mpteqb  6960  fvmptt  6961  fvmptf  6962  fnmptfvd  6986  ralrnmptw  7039  ralrnmpt  7041  fompt  7063  fmptco  7074  f1mpt  7207  offval2  7642  ofrfval2  7643  fimaproj  8077  mptelixpg  8873  dom2lem  8929  mapxpen  9071  xpmapenlem  9072  cnfcom3clem  9614  tcvalg  9645  rankf  9706  infxpenc2lem2  9930  dfac8clem  9942  acni2  9956  acnlem  9958  fin23lem32  10254  axcc2lem  10346  axcc3  10348  domtriomlem  10352  ac6num  10389  konigthlem  10479  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  seqof  13982  seqof2  13983  rlim2  15419  ello1mpt  15444  o1compt  15510  sumrblem  15634  fsumcvg  15635  summolem2a  15638  fsum  15643  fsumcvg2  15650  fsumadd  15663  isummulc2  15685  fsummulc2  15707  fsumrelem  15730  prodrblem  15852  fprodcvg  15853  prodmolem2a  15857  zprod  15860  fprod  15864  fprodmul  15883  fproddiv  15884  iserodd  16763  prmrec  16850  prdsbas3  17401  prdsdsval2  17404  invfuc  17901  yonedalem4c  18200  smndex1n0mnd  18837  gsumconst  19863  prdsgsum  19910  gsumdixp  20254  pwsgprod  20265  evlslem4  22031  elptr2  23518  ptunimpt  23539  ptcldmpt  23558  ptclsg  23559  txcnp  23564  ptcnplem  23565  cnmpt11  23607  cnmpt1t  23609  cnmptk2  23630  xkocnv  23758  flfcnp2  23951  ustn0  24165  utopsnneiplem  24191  ucnima  24224  iccpnfcnv  24898  ovolctb  25447  ovoliunlem1  25459  ovoliun2  25463  ovolshftlem1  25466  ovolscalem1  25470  voliun  25511  ioombl1lem3  25517  ioombl1lem4  25518  uniioombllem2  25540  mbfeqalem1  25598  mbfpos  25608  mbfposr  25609  mbfposb  25610  mbfsup  25621  mbfinf  25622  mbflim  25625  i1fposd  25664  itg1climres  25671  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  itg2split  25706  itg2mono  25710  itg2cnlem1  25718  isibl2  25723  itgmpt  25740  itgeqa  25771  itggt0  25801  itgcn  25802  limcmpt  25840  dvlipcn  25955  lhop2  25976  dvfsumabs  25985  itgparts  26010  itgsubstlem  26011  itgsubst  26012  elplyd  26163  coeeulem  26185  coeeq2  26203  dvply1  26247  plyremlem  26268  ulmss  26362  ulmdvlem1  26365  mtest  26369  itgulm2  26374  radcnvlem1  26378  pserulm  26387  leibpi  26908  rlimcnp  26931  o1cxp  26941  lgamgulmlem2  26996  lgamgulmlem6  27000  lgamgulm2  27002  sqff1o  27148  lgseisenlem2  27343  dchrvmasumlem1  27462  frgrncvvdeqlem5  30378  ubthlem1  30945  cnlnadjlem5  32146  xppreima2  32729  abfmpunirn  32730  aciunf1lem  32740  suppovss  32760  fpwrelmap  32812  nsgmgc  33493  zringfrac  33635  extdgfialglem2  33850  algextdeglem6  33879  xrmulc1cn  34087  esumpcvgval  34235  esumsup  34246  voliune  34386  eulerpartgbij  34529  signsplypnf  34707  wevgblacfn  35303  iscvm  35453  mclsrcl  35755  f1omptsnlem  37537  matunitlindflem2  37814  itg2addnclem  37868  itggt0cn  37887  ftc1anclem5  37894  elrfirn2  42934  eq0rabdioph  43014  monotoddzz  43181  aomclem2  43293  refsumcn  45271  refsum2cnlem1  45278  fvmpt2bd  45410  choicefi  45440  axccdom  45462  fvmpt4  45478  fsumsermpt  45821  fmuldfeqlem1  45824  fmuldfeq  45825  climneg  45852  climdivf  45854  mullimc  45858  idlimc  45868  sumnnodd  45872  neglimc  45887  addlimc  45888  0ellimcdiv  45889  climfveqmpt2  45933  climeqmpt  45937  limsupequzmptlem  45968  liminfvalxr  46023  xlimmnfmpt  46083  xlimpnfmpt  46084  cncfmptssg  46111  cncfshift  46114  icccncfext  46127  cncfiooicclem1  46133  fprodsubrecnncnvlem  46147  fprodaddrecnncnvlem  46149  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnmptdivc  46178  dvnmul  46183  dvnprodlem2  46187  itgsin0pilem1  46190  ibliccsinexp  46191  itgsinexplem1  46194  itgsinexp  46195  ditgeqiooicc  46200  itgsubsticclem  46215  itgioocnicc  46217  stoweidlem2  46242  stoweidlem11  46251  stoweidlem12  46252  stoweidlem16  46256  stoweidlem17  46257  stoweidlem18  46258  stoweidlem19  46259  stoweidlem20  46260  stoweidlem21  46261  stoweidlem22  46262  stoweidlem23  46263  stoweidlem27  46267  stoweidlem31  46271  stoweidlem34  46274  stoweidlem36  46276  stoweidlem40  46280  stoweidlem41  46281  stoweidlem42  46282  stoweidlem48  46288  stoweidlem55  46295  stoweidlem59  46299  stoweidlem62  46302  stirlinglem3  46316  stirlinglem8  46321  stirlinglem14  46327  stirlinglem15  46328  stirlingr  46330  dirkeritg  46342  dirkercncflem2  46344  fourierdlem14  46361  fourierdlem31  46378  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem51  46397  fourierdlem56  46402  fourierdlem60  46406  fourierdlem61  46407  fourierdlem66  46412  fourierdlem70  46416  fourierdlem71  46417  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem77  46423  fourierdlem78  46424  fourierdlem81  46427  fourierdlem83  46429  fourierdlem84  46430  fourierdlem85  46431  fourierdlem87  46433  fourierdlem88  46434  fourierdlem89  46435  fourierdlem91  46437  fourierdlem92  46438  fourierdlem93  46439  fourierdlem95  46441  fourierdlem97  46443  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem112  46458  sqwvfoura  46468  sqwvfourb  46469  fouriersw  46471  elaa2lem  46473  etransclem4  46478  etransclem13  46487  etransclem35  46509  etransclem46  46520  etransclem48  46522  sge0revalmpt  46618  sge0fsummpt  46630  sge0iunmptlemfi  46653  sge0iunmptlemre  46655  sge0ltfirpmpt2  46666  sge0fsummptf  46676  nnfoctbdjlem  46695  iundjiun  46700  meaiunlelem  46708  meaiuninclem  46720  meaiuninc3v  46724  omeiunlempt  46760  carageniuncllem2  46762  caratheodorylem2  46767  0ome  46769  isomenndlem  46770  hoicvr  46788  hoicvrrex  46796  ovn0lem  46805  ovnsubaddlem1  46810  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoilem2  46842  hoicoto2  46845  hoi2toco  46847  ovnlecvr2  46850  ovncvr2  46851  ovnsubadd2lem  46885  ovolval5lem2  46893  ovnovollem1  46896  ovnovollem2  46897  vonioolem1  46920  smfaddlem1  47003  smflimlem2  47012  smflimmpt  47050  smflimsuplem2  47061  smflimsuplem4  47063  smflimsuplem5  47064  smflimsupmpt  47069  smfliminfmpt  47072  smfsupdmmbllem  47084  finfdm  47086  smfinfdmmbllem  47088  setrec2mpt  49938  aacllem  50042