Theorem fvmpt2 6961

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181   I cid 5526  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  fvmptss  6962  fvmpt2d  6963  fvmptd3f  6965  mpteqb  6969  fvmptt  6970  fvmptf  6971  fnmptfvd  6995  ralrnmptw  7048  ralrnmpt  7050  fompt  7072  fmptco  7084  f1mpt  7217  offval2  7652  ofrfval2  7653  fimaproj  8087  mptelixpg  8885  dom2lem  8941  mapxpen  9083  xpmapenlem  9084  cnfcom3clem  9626  tcvalg  9657  rankf  9718  infxpenc2lem2  9942  dfac8clem  9954  acni2  9968  acnlem  9970  fin23lem32  10266  axcc2lem  10358  axcc3  10360  domtriomlem  10364  ac6num  10401  konigthlem  10491  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  seqof  13994  seqof2  13995  rlim2  15431  ello1mpt  15456  o1compt  15522  sumrblem  15646  fsumcvg  15647  summolem2a  15650  fsum  15655  fsumcvg2  15662  fsumadd  15675  isummulc2  15697  fsummulc2  15719  fsumrelem  15742  prodrblem  15864  fprodcvg  15865  prodmolem2a  15869  zprod  15872  fprod  15876  fprodmul  15895  fproddiv  15896  iserodd  16775  prmrec  16862  prdsbas3  17413  prdsdsval2  17416  invfuc  17913  yonedalem4c  18212  smndex1n0mnd  18849  gsumconst  19875  prdsgsum  19922  gsumdixp  20266  pwsgprod  20277  evlslem4  22043  elptr2  23530  ptunimpt  23551  ptcldmpt  23570  ptclsg  23571  txcnp  23576  ptcnplem  23577  cnmpt11  23619  cnmpt1t  23621  cnmptk2  23642  xkocnv  23770  flfcnp2  23963  ustn0  24177  utopsnneiplem  24203  ucnima  24236  iccpnfcnv  24910  ovolctb  25459  ovoliunlem1  25471  ovoliun2  25475  ovolshftlem1  25478  ovolscalem1  25482  voliun  25523  ioombl1lem3  25529  ioombl1lem4  25530  uniioombllem2  25552  mbfeqalem1  25610  mbfpos  25620  mbfposr  25621  mbfposb  25622  mbfsup  25633  mbfinf  25634  mbflim  25637  i1fposd  25676  itg1climres  25683  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2split  25718  itg2mono  25722  itg2cnlem1  25730  isibl2  25735  itgmpt  25752  itgeqa  25783  itggt0  25813  itgcn  25814  limcmpt  25852  dvlipcn  25967  lhop2  25988  dvfsumabs  25997  itgparts  26022  itgsubstlem  26023  itgsubst  26024  elplyd  26175  coeeulem  26197  coeeq2  26215  dvply1  26259  plyremlem  26280  ulmss  26374  ulmdvlem1  26377  mtest  26381  itgulm2  26386  radcnvlem1  26390  pserulm  26399  leibpi  26920  rlimcnp  26943  o1cxp  26953  lgamgulmlem2  27008  lgamgulmlem6  27012  lgamgulm2  27014  sqff1o  27160  lgseisenlem2  27355  dchrvmasumlem1  27474  frgrncvvdeqlem5  30390  ubthlem1  30957  cnlnadjlem5  32158  xppreima2  32740  abfmpunirn  32741  aciunf1lem  32751  suppovss  32770  fpwrelmap  32822  suppgsumssiun  33165  nsgmgc  33504  zringfrac  33646  extdgfialglem2  33870  algextdeglem6  33899  xrmulc1cn  34107  esumpcvgval  34255  esumsup  34266  voliune  34406  eulerpartgbij  34549  signsplypnf  34727  wevgblacfn  35322  iscvm  35472  mclsrcl  35774  f1omptsnlem  37585  matunitlindflem2  37862  itg2addnclem  37916  itggt0cn  37935  ftc1anclem5  37942  elrfirn2  43047  eq0rabdioph  43127  monotoddzz  43294  aomclem2  43406  refsumcn  45384  refsum2cnlem1  45391  fvmpt2bd  45523  choicefi  45552  axccdom  45574  fvmpt4  45590  fsumsermpt  45933  fmuldfeqlem1  45936  fmuldfeq  45937  climneg  45964  climdivf  45966  mullimc  45970  idlimc  45980  sumnnodd  45984  neglimc  45999  addlimc  46000  0ellimcdiv  46001  climfveqmpt2  46045  climeqmpt  46049  limsupequzmptlem  46080  liminfvalxr  46135  xlimmnfmpt  46195  xlimpnfmpt  46196  cncfmptssg  46223  cncfshift  46226  icccncfext  46239  cncfiooicclem1  46245  fprodsubrecnncnvlem  46259  fprodaddrecnncnvlem  46261  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnmptdivc  46290  dvnmul  46295  dvnprodlem2  46299  itgsin0pilem1  46302  ibliccsinexp  46303  itgsinexplem1  46306  itgsinexp  46307  ditgeqiooicc  46312  itgsubsticclem  46327  itgioocnicc  46329  stoweidlem2  46354  stoweidlem11  46363  stoweidlem12  46364  stoweidlem16  46368  stoweidlem17  46369  stoweidlem18  46370  stoweidlem19  46371  stoweidlem20  46372  stoweidlem21  46373  stoweidlem22  46374  stoweidlem23  46375  stoweidlem27  46379  stoweidlem31  46383  stoweidlem34  46386  stoweidlem36  46388  stoweidlem40  46392  stoweidlem41  46393  stoweidlem42  46394  stoweidlem48  46400  stoweidlem55  46407  stoweidlem59  46411  stoweidlem62  46414  stirlinglem3  46428  stirlinglem8  46433  stirlinglem14  46439  stirlinglem15  46440  stirlingr  46442  dirkeritg  46454  dirkercncflem2  46456  fourierdlem14  46473  fourierdlem31  46490  fourierdlem41  46500  fourierdlem48  46506  fourierdlem49  46507  fourierdlem50  46508  fourierdlem51  46509  fourierdlem56  46514  fourierdlem60  46518  fourierdlem61  46519  fourierdlem66  46524  fourierdlem70  46528  fourierdlem71  46529  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem77  46535  fourierdlem78  46536  fourierdlem81  46539  fourierdlem83  46541  fourierdlem84  46542  fourierdlem85  46543  fourierdlem87  46545  fourierdlem88  46546  fourierdlem89  46547  fourierdlem91  46549  fourierdlem92  46550  fourierdlem93  46551  fourierdlem95  46553  fourierdlem97  46555  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem112  46570  sqwvfoura  46580  sqwvfourb  46581  fouriersw  46583  elaa2lem  46585  etransclem4  46590  etransclem13  46599  etransclem35  46621  etransclem46  46632  etransclem48  46634  sge0revalmpt  46730  sge0fsummpt  46742  sge0iunmptlemfi  46765  sge0iunmptlemre  46767  sge0ltfirpmpt2  46778  sge0fsummptf  46788  nnfoctbdjlem  46807  iundjiun  46812  meaiunlelem  46820  meaiuninclem  46832  meaiuninc3v  46836  omeiunlempt  46872  carageniuncllem2  46874  caratheodorylem2  46879  0ome  46881  isomenndlem  46882  hoicvr  46900  hoicvrrex  46908  ovn0lem  46917  ovnsubaddlem1  46922  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoilem2  46954  hoicoto2  46957  hoi2toco  46959  ovnlecvr2  46962  ovncvr2  46963  ovnsubadd2lem  46997  ovolval5lem2  47005  ovnovollem1  47008  ovnovollem2  47009  vonioolem1  47032  smfaddlem1  47115  smflimlem2  47124  smflimmpt  47162  smflimsuplem2  47173  smflimsuplem4  47175  smflimsuplem5  47176  smflimsupmpt  47181  smfliminfmpt  47184  smfsupdmmbllem  47196  finfdm  47198  smfinfdmmbllem  47200  setrec2mpt  50050  aacllem  50154