Theorem fvmpt2 7008

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5197   I cid 5560  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551

This theorem is used by:  fvmptss  7009  fvmpt2d  7010  fvmptd3f  7012  mpteqb  7016  fvmptt  7017  fvmptf  7018  fnmptfvd  7043  ralrnmptw  7096  ralrnmpt  7098  fompt  7120  fmptco  7132  f1mpt  7266  offval2  7707  ofrfval2  7708  fimaproj  8140  mptelixpg  8942  dom2lem  8998  mapxpen  9141  xpmapenlem  9142  cnfcom3clem  9684  tcvalg  9715  rankf  9776  infxpenc2lem2  10023  dfac8clem  10035  acni2  10049  acnlem  10051  fin23lem32  10346  axcc2lem  10438  axcc3  10440  domtriomlem  10444  ac6num  10481  konigthlem  10571  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  seqof  14115  seqof2  14116  rlim2  15573  ello1mpt  15598  o1compt  15664  sumrblem  15788  fsumcvg  15789  summolem2a  15792  fsum  15797  fsumcvg2  15804  fsumadd  15817  isummulc2  15839  fsummulc2  15861  fsumrelem  15885  prodrblem  16009  fprodcvg  16010  prodmolem2a  16014  zprod  16017  fprod  16021  fprodmul  16040  fproddiv  16041  iserodd  16920  prmrec  17007  prdsbas3  17559  prdsdsval2  17562  invfuc  18059  yonedalem4c  18358  smndex1n0mnd  19005  gsumconst  20035  prdsgsum  20082  gsumdixp  20433  pwsgprod  20444  evlslem4  22264  elptr2  23768  ptunimpt  23789  ptcldmpt  23808  ptclsg  23809  txcnp  23814  ptcnplem  23815  cnmpt11  23857  cnmpt1t  23859  cnmptk2  23880  xkocnv  24008  flfcnp2  24201  ustn0  24415  utopsnneiplem  24441  ucnima  24474  iccpnfcnv  25140  ovolctb  25686  ovoliunlem1  25698  ovoliun2  25702  ovolshftlem1  25705  ovolscalem1  25709  voliun  25750  ioombl1lem3  25756  ioombl1lem4  25757  uniioombllem2  25779  mbfeqalem1  25837  mbfpos  25847  mbfposr  25848  mbfposb  25849  mbfsup  25860  mbfinf  25861  mbflim  25864  i1fposd  25903  itg1climres  25910  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1fseqlem6  25916  itg2split  25945  itg2mono  25949  itg2cnlem1  25957  isibl2  25962  itgmpt  25979  itgeqa  26010  itggt0  26040  itgcn  26041  limcmpt  26079  dvlipcn  26190  lhop2  26211  dvfsumabs  26219  itgparts  26243  itgsubstlem  26244  itgsubst  26245  elplyd  26396  coeeulem  26418  coeeq2  26436  dvply1  26482  plyremlem  26502  ulmss  26597  ulmdvlem1  26600  mtest  26604  itgulm2  26609  radcnvlem1  26613  pserulm  26622  leibpi  27144  rlimcnp  27167  o1cxp  27176  lgamgulmlem2  27231  lgamgulmlem6  27235  lgamgulm2  27237  sqff1o  27383  lgseisenlem2  27577  dchrvmasumlem1  27696  frgrncvvdeqlem5  30691  ubthlem1  31259  cnlnadjlem5  32460  xppreima2  33033  abfmpunirn  33034  aciunf1lem  33044  suppovss  33063  fpwrelmap  33115  suppgsumssiun  33423  nsgmgc  33752  zringfrac  33875  extdgfialglem2  34114  algextdeglem6  34143  xrmulc1cn  34351  esumpcvgval  34499  esumsup  34510  voliune  34650  eulerpartgbij  34793  signsplypnf  34968  wevgblacfn  35618  iscvm  35771  mclsrcl  36073  f1omptsnlem  38022  matunitlindflem2  38308  itg2addnclem  38362  itggt0cn  38381  ftc1anclem5  38388  elrfirn2  43467  eq0rabdioph  43547  monotoddzz  43710  aomclem2  43822  refsumcn  45790  refsum2cnlem1  45797  fvmpt2bd  45928  choicefi  45957  axccdom  45978  fvmpt4  45993  fsumsermpt  46335  fmuldfeqlem1  46338  fmuldfeq  46339  climneg  46366  climdivf  46368  mullimc  46372  idlimc  46382  sumnnodd  46386  neglimc  46401  addlimc  46402  0ellimcdiv  46403  climfveqmpt2  46447  climeqmpt  46451  limsupequzmptlem  46482  liminfvalxr  46537  xlimmnfmpt  46597  xlimpnfmpt  46598  cncfmptssg  46625  cncfshift  46628  icccncfext  46641  cncfiooicclem1  46647  fprodsubrecnncnvlem  46661  fprodaddrecnncnvlem  46663  ioodvbdlimc1lem2  46686  ioodvbdlimc2lem  46688  dvnmptdivc  46692  dvnmul  46697  dvnprodlem2  46701  itgsin0pilem1  46704  ibliccsinexp  46705  itgsinexplem1  46708  itgsinexp  46709  ditgeqiooicc  46714  itgsubsticclem  46729  itgioocnicc  46731  stoweidlem2  46756  stoweidlem11  46765  stoweidlem12  46766  stoweidlem16  46770  stoweidlem17  46771  stoweidlem18  46772  stoweidlem19  46773  stoweidlem20  46774  stoweidlem21  46775  stoweidlem22  46776  stoweidlem23  46777  stoweidlem27  46781  stoweidlem31  46785  stoweidlem34  46788  stoweidlem36  46790  stoweidlem40  46794  stoweidlem41  46795  stoweidlem42  46796  stoweidlem48  46802  stoweidlem55  46809  stoweidlem59  46813  stoweidlem62  46816  stirlinglem3  46830  stirlinglem8  46835  stirlinglem14  46841  stirlinglem15  46842  stirlingr  46844  dirkeritg  46856  dirkercncflem2  46858  fourierdlem14  46875  fourierdlem31  46892  fourierdlem41  46902  fourierdlem48  46908  fourierdlem49  46909  fourierdlem50  46910  fourierdlem51  46911  fourierdlem56  46916  fourierdlem60  46920  fourierdlem61  46921  fourierdlem66  46926  fourierdlem70  46930  fourierdlem71  46931  fourierdlem73  46933  fourierdlem74  46934  fourierdlem75  46935  fourierdlem76  46936  fourierdlem77  46937  fourierdlem78  46938  fourierdlem81  46941  fourierdlem83  46943  fourierdlem84  46944  fourierdlem85  46945  fourierdlem87  46947  fourierdlem88  46948  fourierdlem89  46949  fourierdlem91  46951  fourierdlem92  46952  fourierdlem93  46953  fourierdlem95  46955  fourierdlem97  46957  fourierdlem101  46961  fourierdlem103  46963  fourierdlem104  46964  fourierdlem111  46971  fourierdlem112  46972  sqwvfoura  46982  sqwvfourb  46983  fouriersw  46985  elaa2lem  46987  etransclem4  46992  etransclem13  47001  etransclem35  47023  etransclem46  47034  etransclem48  47036  sge0revalmpt  47132  sge0fsummpt  47144  sge0iunmptlemfi  47167  sge0iunmptlemre  47169  sge0ltfirpmpt2  47180  sge0fsummptf  47190  nnfoctbdjlem  47209  iundjiun  47214  meaiunlelem  47222  meaiuninclem  47234  meaiuninc3v  47238  omeiunlempt  47274  carageniuncllem2  47276  caratheodorylem2  47281  0ome  47283  isomenndlem  47284  hoicvr  47302  hoicvrrex  47310  ovn0lem  47319  ovnsubaddlem1  47324  hoidmvlelem2  47350  hoidmvlelem3  47351  ovnhoilem2  47356  hoicoto2  47359  hoi2toco  47361  ovnlecvr2  47364  ovncvr2  47365  ovnsubadd2lem  47399  ovolval5lem2  47407  ovnovollem1  47410  ovnovollem2  47411  vonioolem1  47434  smfaddlem1  47517  smflimlem2  47526  smflimmpt  47564  smflimsuplem2  47575  smflimsuplem4  47577  smflimsuplem5  47578  smflimsupmpt  47583  smfliminfmpt  47586  smfsupdmmbllem  47598  finfdm  47600  smfinfdmmbllem  47602  setrec2mpt  50515  aacllem  50661