Theorem fvmpt2 6954

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160   I cid 5519  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptss  6955  fvmpt2d  6956  fvmptd3f  6958  mpteqb  6962  fvmptt  6963  fvmptf  6964  fnmptfvd  6989  ralrnmptw  7042  ralrnmpt  7044  fompt  7066  fmptco  7078  f1mpt  7212  offval2  7647  ofrfval2  7648  fimaproj  8082  mptelixpg  8880  dom2lem  8936  mapxpen  9078  xpmapenlem  9079  cnfcom3clem  9624  tcvalg  9655  rankf  9716  infxpenc2lem2  9940  dfac8clem  9952  acni2  9966  acnlem  9968  fin23lem32  10264  axcc2lem  10356  axcc3  10358  domtriomlem  10362  ac6num  10399  konigthlem  10489  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  seqof  14019  seqof2  14020  rlim2  15456  ello1mpt  15481  o1compt  15547  sumrblem  15671  fsumcvg  15672  summolem2a  15675  fsum  15680  fsumcvg2  15687  fsumadd  15700  isummulc2  15722  fsummulc2  15744  fsumrelem  15768  prodrblem  15892  fprodcvg  15893  prodmolem2a  15897  zprod  15900  fprod  15904  fprodmul  15923  fproddiv  15924  iserodd  16804  prmrec  16891  prdsbas3  17442  prdsdsval2  17445  invfuc  17942  yonedalem4c  18241  smndex1n0mnd  18881  gsumconst  19907  prdsgsum  19954  gsumdixp  20296  pwsgprod  20307  evlslem4  22059  elptr2  23564  ptunimpt  23585  ptcldmpt  23604  ptclsg  23605  txcnp  23610  ptcnplem  23611  cnmpt11  23653  cnmpt1t  23655  cnmptk2  23676  xkocnv  23804  flfcnp2  23997  ustn0  24211  utopsnneiplem  24237  ucnima  24270  iccpnfcnv  24936  ovolctb  25482  ovoliunlem1  25494  ovoliun2  25498  ovolshftlem1  25501  ovolscalem1  25505  voliun  25546  ioombl1lem3  25552  ioombl1lem4  25553  uniioombllem2  25575  mbfeqalem1  25633  mbfpos  25643  mbfposr  25644  mbfposb  25645  mbfsup  25656  mbfinf  25657  mbflim  25660  i1fposd  25699  itg1climres  25706  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  itg2split  25741  itg2mono  25745  itg2cnlem1  25753  isibl2  25758  itgmpt  25775  itgeqa  25806  itggt0  25836  itgcn  25837  limcmpt  25875  dvlipcn  25986  lhop2  26007  dvfsumabs  26015  itgparts  26039  itgsubstlem  26040  itgsubst  26041  elplyd  26192  coeeulem  26214  coeeq2  26232  dvply1  26275  plyremlem  26295  ulmss  26387  ulmdvlem1  26390  mtest  26394  itgulm2  26399  radcnvlem1  26403  pserulm  26412  leibpi  26931  rlimcnp  26954  o1cxp  26963  lgamgulmlem2  27018  lgamgulmlem6  27022  lgamgulm2  27024  sqff1o  27170  lgseisenlem2  27364  dchrvmasumlem1  27483  frgrncvvdeqlem5  30398  ubthlem1  30966  cnlnadjlem5  32167  xppreima2  32750  abfmpunirn  32751  aciunf1lem  32761  suppovss  32780  fpwrelmap  32832  suppgsumssiun  33160  nsgmgc  33502  zringfrac  33644  extdgfialglem2  33884  algextdeglem6  33913  xrmulc1cn  34121  esumpcvgval  34269  esumsup  34280  voliune  34420  eulerpartgbij  34563  signsplypnf  34741  wevgblacfn  35344  iscvm  35494  mclsrcl  35796  f1omptsnlem  37705  matunitlindflem2  37991  itg2addnclem  38045  itggt0cn  38064  ftc1anclem5  38071  elrfirn2  43152  eq0rabdioph  43232  monotoddzz  43395  aomclem2  43507  refsumcn  45485  refsum2cnlem1  45492  fvmpt2bd  45624  choicefi  45653  axccdom  45674  fvmpt4  45689  fsumsermpt  46031  fmuldfeqlem1  46034  fmuldfeq  46035  climneg  46062  climdivf  46064  mullimc  46068  idlimc  46078  sumnnodd  46082  neglimc  46097  addlimc  46098  0ellimcdiv  46099  climfveqmpt2  46143  climeqmpt  46147  limsupequzmptlem  46178  liminfvalxr  46233  xlimmnfmpt  46293  xlimpnfmpt  46294  cncfmptssg  46321  cncfshift  46324  icccncfext  46337  cncfiooicclem1  46343  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnmptdivc  46388  dvnmul  46393  dvnprodlem2  46397  itgsin0pilem1  46400  ibliccsinexp  46401  itgsinexplem1  46404  itgsinexp  46405  ditgeqiooicc  46410  itgsubsticclem  46425  itgioocnicc  46427  stoweidlem2  46452  stoweidlem11  46461  stoweidlem12  46462  stoweidlem16  46466  stoweidlem17  46467  stoweidlem18  46468  stoweidlem19  46469  stoweidlem20  46470  stoweidlem21  46471  stoweidlem22  46472  stoweidlem23  46473  stoweidlem27  46477  stoweidlem31  46481  stoweidlem34  46484  stoweidlem36  46486  stoweidlem40  46490  stoweidlem41  46491  stoweidlem42  46492  stoweidlem48  46498  stoweidlem55  46505  stoweidlem59  46509  stoweidlem62  46512  stirlinglem3  46526  stirlinglem8  46531  stirlinglem14  46537  stirlinglem15  46538  stirlingr  46540  dirkeritg  46552  dirkercncflem2  46554  fourierdlem14  46571  fourierdlem31  46588  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem56  46612  fourierdlem60  46616  fourierdlem61  46617  fourierdlem66  46622  fourierdlem70  46626  fourierdlem71  46627  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem77  46633  fourierdlem78  46634  fourierdlem81  46637  fourierdlem83  46639  fourierdlem84  46640  fourierdlem85  46641  fourierdlem87  46643  fourierdlem88  46644  fourierdlem89  46645  fourierdlem91  46647  fourierdlem92  46648  fourierdlem93  46649  fourierdlem95  46651  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  elaa2lem  46683  etransclem4  46688  etransclem13  46697  etransclem35  46719  etransclem46  46730  etransclem48  46732  sge0revalmpt  46828  sge0fsummpt  46840  sge0iunmptlemfi  46863  sge0iunmptlemre  46865  sge0ltfirpmpt2  46876  sge0fsummptf  46886  nnfoctbdjlem  46905  iundjiun  46910  meaiunlelem  46918  meaiuninclem  46930  meaiuninc3v  46934  omeiunlempt  46970  carageniuncllem2  46972  caratheodorylem2  46977  0ome  46979  isomenndlem  46980  hoicvr  46998  hoicvrrex  47006  ovn0lem  47015  ovnsubaddlem1  47020  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem2  47052  hoicoto2  47055  hoi2toco  47057  ovnlecvr2  47060  ovncvr2  47061  ovnsubadd2lem  47095  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  vonioolem1  47130  smfaddlem1  47213  smflimlem2  47222  smflimmpt  47260  smflimsuplem2  47271  smflimsuplem4  47273  smflimsuplem5  47274  smflimsupmpt  47279  smfliminfmpt  47282  smfsupdmmbllem  47294  finfdm  47296  smfinfdmmbllem  47298  setrec2mpt  50194  aacllem  50298