Theorem fvmpt2 7007

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5231   I cid 5573  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fv 6549

This theorem is referenced by:  fvmptss  7008  fvmpt2d  7009  fvmptd3f  7011  mpteqb  7015  fvmptt  7016  fvmptf  7017  fnmptfvd  7040  ralrnmptw  7093  ralrnmpt  7095  fmptco  7124  f1mpt  7257  offval2  7687  ofrfval2  7688  fimaproj  8118  mptelixpg  8926  dom2lem  8985  mapxpen  9140  xpmapenlem  9141  cnfcom3clem  9697  tcvalg  9730  rankf  9786  infxpenc2lem2  10012  dfac8clem  10024  acni2  10038  acnlem  10040  fin23lem32  10336  axcc2lem  10428  axcc3  10430  domtriomlem  10434  ac6num  10471  konigthlem  10560  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem5  12962  seqof  14022  seqof2  14023  rlim2  15437  ello1mpt  15462  o1compt  15528  sumrblem  15654  fsumcvg  15655  summolem2a  15658  fsum  15663  fsumcvg2  15670  fsumadd  15683  isummulc2  15705  fsummulc2  15727  fsumrelem  15750  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  zprod  15878  fprod  15882  fprodmul  15901  fproddiv  15902  iserodd  16765  prmrec  16852  prdsbas3  17424  prdsdsval2  17427  invfuc  17924  yonedalem4c  18227  smndex1n0mnd  18790  gsumconst  19797  prdsgsum  19844  gsumdixp  20125  evlslem4  21629  elptr2  23070  ptunimpt  23091  ptcldmpt  23110  ptclsg  23111  txcnp  23116  ptcnplem  23117  cnmpt11  23159  cnmpt1t  23161  cnmptk2  23182  xkocnv  23310  flfcnp2  23503  ustn0  23717  utopsnneiplem  23744  ucnima  23778  iccpnfcnv  24452  ovolctb  24999  ovoliunlem1  25011  ovoliun2  25015  ovolshftlem1  25018  ovolscalem1  25022  voliun  25063  ioombl1lem3  25069  ioombl1lem4  25070  uniioombllem2  25092  mbfeqalem1  25150  mbfpos  25160  mbfposr  25161  mbfposb  25162  mbfsup  25173  mbfinf  25174  mbflim  25177  i1fposd  25217  itg1climres  25224  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2split  25259  itg2mono  25263  itg2cnlem1  25271  isibl2  25276  itgmpt  25292  itgeqa  25323  itggt0  25353  itgcn  25354  limcmpt  25392  dvlipcn  25503  lhop2  25524  dvfsumabs  25532  itgparts  25556  itgsubstlem  25557  itgsubst  25558  elplyd  25708  coeeulem  25730  coeeq2  25748  dvply1  25789  plyremlem  25809  ulmss  25901  ulmdvlem1  25904  mtest  25908  itgulm2  25913  radcnvlem1  25917  pserulm  25926  leibpi  26437  rlimcnp  26460  o1cxp  26469  lgamgulmlem2  26524  lgamgulmlem6  26528  lgamgulm2  26530  sqff1o  26676  lgseisenlem2  26869  dchrvmasumlem1  26988  frgrncvvdeqlem5  29546  ubthlem1  30111  cnlnadjlem5  31312  xppreima2  31864  abfmpunirn  31865  aciunf1lem  31875  suppovss  31894  fpwrelmap  31946  nsgmgc  32512  xrmulc1cn  32899  esumpcvgval  33065  esumsup  33076  voliune  33216  eulerpartgbij  33360  signsplypnf  33550  iscvm  34239  mclsrcl  34541  f1omptsnlem  36206  matunitlindflem2  36474  itg2addnclem  36528  itggt0cn  36547  ftc1anclem5  36554  pwsgprod  41112  elrfirn2  41420  eq0rabdioph  41500  monotoddzz  41668  aomclem2  41783  refsumcn  43700  refsum2cnlem1  43707  fvmpt2bd  43852  fompt  43876  choicefi  43885  axccdom  43907  fvmpt4  43927  fsumsermpt  44282  fmuldfeqlem1  44285  fmuldfeq  44286  climneg  44313  climdivf  44315  mullimc  44319  idlimc  44329  sumnnodd  44333  neglimc  44350  addlimc  44351  0ellimcdiv  44352  climfveqmpt2  44396  climeqmpt  44400  limsupequzmptlem  44431  liminfvalxr  44486  xlimmnfmpt  44546  xlimpnfmpt  44547  cncfmptssg  44574  cncfshift  44577  icccncfext  44590  cncfiooicclem1  44596  fprodsubrecnncnvlem  44610  fprodaddrecnncnvlem  44612  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnmptdivc  44641  dvnmul  44646  dvnprodlem2  44650  itgsin0pilem1  44653  ibliccsinexp  44654  itgsinexplem1  44657  itgsinexp  44658  ditgeqiooicc  44663  itgsubsticclem  44678  itgioocnicc  44680  stoweidlem2  44705  stoweidlem11  44714  stoweidlem12  44715  stoweidlem16  44719  stoweidlem17  44720  stoweidlem18  44721  stoweidlem19  44722  stoweidlem20  44723  stoweidlem21  44724  stoweidlem22  44725  stoweidlem23  44726  stoweidlem27  44730  stoweidlem31  44734  stoweidlem34  44737  stoweidlem36  44739  stoweidlem40  44743  stoweidlem41  44744  stoweidlem42  44745  stoweidlem48  44751  stoweidlem55  44758  stoweidlem59  44762  stoweidlem62  44765  stirlinglem3  44779  stirlinglem8  44784  stirlinglem14  44790  stirlinglem15  44791  stirlingr  44793  dirkeritg  44805  dirkercncflem2  44807  fourierdlem14  44824  fourierdlem31  44841  fourierdlem41  44851  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem51  44860  fourierdlem56  44865  fourierdlem60  44869  fourierdlem61  44870  fourierdlem66  44875  fourierdlem70  44879  fourierdlem71  44880  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem77  44886  fourierdlem78  44887  fourierdlem81  44890  fourierdlem83  44892  fourierdlem84  44893  fourierdlem85  44894  fourierdlem87  44896  fourierdlem88  44897  fourierdlem89  44898  fourierdlem91  44900  fourierdlem92  44901  fourierdlem93  44902  fourierdlem95  44904  fourierdlem97  44906  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  sqwvfoura  44931  sqwvfourb  44932  fouriersw  44934  elaa2lem  44936  etransclem4  44941  etransclem13  44950  etransclem35  44972  etransclem46  44983  etransclem48  44985  sge0revalmpt  45081  sge0fsummpt  45093  sge0iunmptlemfi  45116  sge0iunmptlemre  45118  sge0ltfirpmpt2  45129  sge0fsummptf  45139  nnfoctbdjlem  45158  iundjiun  45163  meaiunlelem  45171  meaiuninclem  45183  meaiuninc3v  45187  omeiunlempt  45223  carageniuncllem2  45225  caratheodorylem2  45230  0ome  45232  isomenndlem  45233  hoicvr  45251  hoicvrrex  45259  ovn0lem  45268  ovnsubaddlem1  45273  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem2  45305  hoicoto2  45308  hoi2toco  45310  ovnlecvr2  45313  ovncvr2  45314  ovnsubadd2lem  45348  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  vonioolem1  45383  smfaddlem1  45466  smflimlem2  45475  smflimmpt  45513  smfinfmpt  45522  smflimsuplem2  45524  smflimsuplem4  45526  smflimsuplem5  45527  smflimsupmpt  45532  smfliminfmpt  45535  smfsupdmmbllem  45547  finfdm  45549  smfinfdmmbllem  45551  setrec2mpt  47696  aacllem  47802