Theorem fvmpt2 6552

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ↦ cmpt 4965   I cid 5260  ‘cfv 6135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fv 6143

This theorem is referenced by:  fvmptss  6553  fvmpt2d  6554  fvmptd3f  6556  mpteqb  6560  fvmptt  6561  fvmptf  6562  fnmptfvd  6583  ralrnmpt  6632  fmptco  6661  f1mpt  6790  offval2  7191  ofrfval2  7192  mptelixpg  8231  dom2lem  8281  mapxpen  8414  xpmapenlem  8415  cnfcom3clem  8899  tcvalg  8911  rankf  8954  infxpenc2lem2  9176  dfac8clem  9188  acni2  9202  acnlem  9204  fin23lem32  9501  axcc2lem  9593  axcc3  9595  domtriomlem  9599  ac6num  9636  konigthlem  9725  rpnnen1lem1  12125  rpnnen1lem3  12126  rpnnen1lem5  12128  seqof  13176  seqof2  13177  rlim2  14635  ello1mpt  14660  o1compt  14726  sumrblem  14849  fsumcvg  14850  summolem2a  14853  fsum  14858  fsumcvg2  14865  fsumadd  14877  isummulc2  14898  fsummulc2  14920  fsumrelem  14943  prodrblem  15062  fprodcvg  15063  prodmolem2a  15067  zprod  15070  fprod  15074  fprodmul  15093  fproddiv  15094  iserodd  15944  prmrec  16030  prdsbas3  16527  prdsdsval2  16530  invfuc  17019  yonedalem4c  17303  gsumconst  18720  prdsgsum  18763  gsumdixp  18996  evlslem4  19904  elptr2  21786  ptunimpt  21807  ptcldmpt  21826  ptclsg  21827  txcnp  21832  ptcnplem  21833  cnmpt11  21875  cnmpt1t  21877  cnmptk2  21898  xkocnv  22026  flfcnp2  22219  ustn0  22432  utopsnneiplem  22459  ucnima  22493  iccpnfcnv  23151  ovolctb  23694  ovoliunlem1  23706  ovoliun2  23710  ovolshftlem1  23713  ovolscalem1  23717  voliun  23758  ioombl1lem3  23764  ioombl1lem4  23765  uniioombllem2  23787  mbfeqalem1  23845  mbfpos  23855  mbfposr  23856  mbfposb  23857  mbfsup  23868  mbfinf  23869  mbflim  23872  i1fposd  23911  itg1climres  23918  mbfi1fseqlem4  23922  mbfi1fseqlem5  23923  mbfi1fseqlem6  23924  itg2split  23953  itg2mono  23957  itg2cnlem1  23965  isibl2  23970  itgmpt  23986  itgeqa  24017  itggt0  24045  itgcn  24046  limcmpt  24084  dvlipcn  24194  lhop2  24215  dvfsumabs  24223  itgparts  24247  itgsubstlem  24248  itgsubst  24249  elplyd  24395  coeeulem  24417  coeeq2  24435  dvply1  24476  plyremlem  24496  ulmss  24588  ulmdvlem1  24591  mtest  24595  itgulm2  24600  radcnvlem1  24604  pserulm  24613  leibpi  25121  rlimcnp  25144  o1cxp  25153  lgamgulmlem2  25208  lgamgulmlem6  25212  lgamgulm2  25214  sqff1o  25360  lgseisenlem2  25553  dchrvmasumlem1  25636  frgrncvvdeqlem5  27711  ubthlem1  28298  cnlnadjlem5  29502  xppreima2  30015  abfmpunirn  30017  aciunf1lem  30027  fpwrelmap  30074  fimaproj  30498  xrmulc1cn  30574  esumpcvgval  30738  esumsup  30749  voliune  30890  eulerpartgbij  31032  signsplypnf  31227  iscvm  31840  mclsrcl  32057  f1omptsnlem  33779  matunitlindflem2  34032  itg2addnclem  34086  itggt0cn  34107  ftc1anclem5  34114  elrfirn2  38219  eq0rabdioph  38300  monotoddzz  38467  aomclem2  38584  refsumcn  40122  refsum2cnlem1  40129  fvmpt2bd  40274  fompt  40302  choicefi  40313  axccdom  40337  fvmpt4  40361  fsumsermpt  40719  fmuldfeqlem1  40722  fmuldfeq  40723  climneg  40750  climdivf  40752  mullimc  40756  idlimc  40766  sumnnodd  40770  neglimc  40787  addlimc  40788  0ellimcdiv  40789  climfveqmpt2  40833  climeqmpt  40837  limsupequzmptlem  40868  liminfvalxr  40923  xlimmnfmpt  40983  xlimpnfmpt  40984  cncfmptssg  41011  cncfshift  41015  icccncfext  41028  cncfiooicclem1  41034  fprodsubrecnncnvlem  41049  fprodaddrecnncnvlem  41051  ioodvbdlimc1lem2  41075  ioodvbdlimc2lem  41077  dvnmptdivc  41081  dvnmul  41086  dvnprodlem2  41090  itgsin0pilem1  41093  ibliccsinexp  41094  itgsinexplem1  41097  itgsinexp  41098  ditgeqiooicc  41103  itgsubsticclem  41118  itgioocnicc  41120  stoweidlem2  41146  stoweidlem11  41155  stoweidlem12  41156  stoweidlem16  41160  stoweidlem17  41161  stoweidlem18  41162  stoweidlem19  41163  stoweidlem20  41164  stoweidlem21  41165  stoweidlem22  41166  stoweidlem23  41167  stoweidlem27  41171  stoweidlem31  41175  stoweidlem34  41178  stoweidlem36  41180  stoweidlem40  41184  stoweidlem41  41185  stoweidlem42  41186  stoweidlem48  41192  stoweidlem55  41199  stoweidlem59  41203  stoweidlem62  41206  stirlinglem3  41220  stirlinglem8  41225  stirlinglem14  41231  stirlinglem15  41232  stirlingr  41234  dirkeritg  41246  dirkercncflem2  41248  fourierdlem14  41265  fourierdlem31  41282  fourierdlem41  41292  fourierdlem48  41298  fourierdlem49  41299  fourierdlem50  41300  fourierdlem51  41301  fourierdlem56  41306  fourierdlem60  41310  fourierdlem61  41311  fourierdlem66  41316  fourierdlem70  41320  fourierdlem71  41321  fourierdlem73  41323  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem77  41327  fourierdlem78  41328  fourierdlem81  41331  fourierdlem83  41333  fourierdlem84  41334  fourierdlem85  41335  fourierdlem87  41337  fourierdlem88  41338  fourierdlem89  41339  fourierdlem91  41341  fourierdlem92  41342  fourierdlem93  41343  fourierdlem95  41345  fourierdlem97  41347  fourierdlem101  41351  fourierdlem103  41353  fourierdlem104  41354  fourierdlem111  41361  fourierdlem112  41362  sqwvfoura  41372  sqwvfourb  41373  fouriersw  41375  elaa2lem  41377  etransclem4  41382  etransclem13  41391  etransclem35  41413  etransclem46  41424  etransclem48  41426  sge0revalmpt  41519  sge0fsummpt  41531  sge0iunmptlemfi  41554  sge0iunmptlemre  41556  sge0ltfirpmpt2  41567  sge0fsummptf  41577  nnfoctbdjlem  41596  iundjiun  41601  meaiunlelem  41609  meaiuninclem  41621  meaiuninc3v  41625  omeiunlempt  41661  carageniuncllem2  41663  caratheodorylem2  41668  0ome  41670  isomenndlem  41671  hoicvr  41689  hoicvrrex  41697  ovn0lem  41706  ovnsubaddlem1  41711  hoidmvlelem2  41737  hoidmvlelem3  41738  ovnhoilem2  41743  hoicoto2  41746  hoi2toco  41748  ovnlecvr2  41751  ovncvr2  41752  ovnsubadd2lem  41786  ovolval5lem2  41794  ovnovollem1  41797  ovnovollem2  41798  vonioolem1  41821  smfaddlem1  41898  smflimlem2  41907  smflimmpt  41943  smfsupmpt  41948  smfinfmpt  41952  smflimsuplem2  41954  smflimsuplem4  41956  smflimsuplem5  41957  smflimsupmpt  41962  smfliminfmpt  41965  aacllem  43653