Theorem fvmpt2 6979

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188   I cid 5532  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvmptss  6980  fvmpt2d  6981  fvmptd3f  6983  mpteqb  6987  fvmptt  6988  fvmptf  6989  fnmptfvd  7013  ralrnmptw  7066  ralrnmpt  7068  fompt  7090  fmptco  7101  f1mpt  7236  offval2  7673  ofrfval2  7674  fimaproj  8114  mptelixpg  8908  dom2lem  8963  mapxpen  9107  xpmapenlem  9108  cnfcom3clem  9658  tcvalg  9691  rankf  9747  infxpenc2lem2  9973  dfac8clem  9985  acni2  9999  acnlem  10001  fin23lem32  10297  axcc2lem  10389  axcc3  10391  domtriomlem  10395  ac6num  10432  konigthlem  10521  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  seqof  14024  seqof2  14025  rlim2  15462  ello1mpt  15487  o1compt  15553  sumrblem  15677  fsumcvg  15678  summolem2a  15681  fsum  15686  fsumcvg2  15693  fsumadd  15706  isummulc2  15728  fsummulc2  15750  fsumrelem  15773  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  fprod  15907  fprodmul  15926  fproddiv  15927  iserodd  16806  prmrec  16893  prdsbas3  17444  prdsdsval2  17447  invfuc  17939  yonedalem4c  18238  smndex1n0mnd  18839  gsumconst  19864  prdsgsum  19911  gsumdixp  20228  evlslem4  21983  elptr2  23461  ptunimpt  23482  ptcldmpt  23501  ptclsg  23502  txcnp  23507  ptcnplem  23508  cnmpt11  23550  cnmpt1t  23552  cnmptk2  23573  xkocnv  23701  flfcnp2  23894  ustn0  24108  utopsnneiplem  24135  ucnima  24168  iccpnfcnv  24842  ovolctb  25391  ovoliunlem1  25403  ovoliun2  25407  ovolshftlem1  25410  ovolscalem1  25414  voliun  25455  ioombl1lem3  25461  ioombl1lem4  25462  uniioombllem2  25484  mbfeqalem1  25542  mbfpos  25552  mbfposr  25553  mbfposb  25554  mbfsup  25565  mbfinf  25566  mbflim  25569  i1fposd  25608  itg1climres  25615  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2split  25650  itg2mono  25654  itg2cnlem1  25662  isibl2  25667  itgmpt  25684  itgeqa  25715  itggt0  25745  itgcn  25746  limcmpt  25784  dvlipcn  25899  lhop2  25920  dvfsumabs  25929  itgparts  25954  itgsubstlem  25955  itgsubst  25956  elplyd  26107  coeeulem  26129  coeeq2  26147  dvply1  26191  plyremlem  26212  ulmss  26306  ulmdvlem1  26309  mtest  26313  itgulm2  26318  radcnvlem1  26322  pserulm  26331  leibpi  26852  rlimcnp  26875  o1cxp  26885  lgamgulmlem2  26940  lgamgulmlem6  26944  lgamgulm2  26946  sqff1o  27092  lgseisenlem2  27287  dchrvmasumlem1  27406  frgrncvvdeqlem5  30232  ubthlem1  30799  cnlnadjlem5  32000  xppreima2  32575  abfmpunirn  32576  aciunf1lem  32586  suppovss  32604  fpwrelmap  32656  nsgmgc  33383  zringfrac  33525  algextdeglem6  33712  xrmulc1cn  33920  esumpcvgval  34068  esumsup  34079  voliune  34219  eulerpartgbij  34363  signsplypnf  34541  wevgblacfn  35096  iscvm  35246  mclsrcl  35548  f1omptsnlem  37324  matunitlindflem2  37611  itg2addnclem  37665  itggt0cn  37684  ftc1anclem5  37691  pwsgprod  42532  elrfirn2  42684  eq0rabdioph  42764  monotoddzz  42932  aomclem2  43044  refsumcn  45024  refsum2cnlem1  45031  fvmpt2bd  45164  choicefi  45194  axccdom  45216  fvmpt4  45232  fsumsermpt  45577  fmuldfeqlem1  45580  fmuldfeq  45581  climneg  45608  climdivf  45610  mullimc  45614  idlimc  45624  sumnnodd  45628  neglimc  45645  addlimc  45646  0ellimcdiv  45647  climfveqmpt2  45691  climeqmpt  45695  limsupequzmptlem  45726  liminfvalxr  45781  xlimmnfmpt  45841  xlimpnfmpt  45842  cncfmptssg  45869  cncfshift  45872  icccncfext  45885  cncfiooicclem1  45891  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmptdivc  45936  dvnmul  45941  dvnprodlem2  45945  itgsin0pilem1  45948  ibliccsinexp  45949  itgsinexplem1  45952  itgsinexp  45953  ditgeqiooicc  45958  itgsubsticclem  45973  itgioocnicc  45975  stoweidlem2  46000  stoweidlem11  46009  stoweidlem12  46010  stoweidlem16  46014  stoweidlem17  46015  stoweidlem18  46016  stoweidlem19  46017  stoweidlem20  46018  stoweidlem21  46019  stoweidlem22  46020  stoweidlem23  46021  stoweidlem27  46025  stoweidlem31  46029  stoweidlem34  46032  stoweidlem36  46034  stoweidlem40  46038  stoweidlem41  46039  stoweidlem42  46040  stoweidlem48  46046  stoweidlem55  46053  stoweidlem59  46057  stoweidlem62  46060  stirlinglem3  46074  stirlinglem8  46079  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  dirkeritg  46100  dirkercncflem2  46102  fourierdlem14  46119  fourierdlem31  46136  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem56  46160  fourierdlem60  46164  fourierdlem61  46165  fourierdlem66  46170  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem77  46181  fourierdlem78  46182  fourierdlem81  46185  fourierdlem83  46187  fourierdlem84  46188  fourierdlem85  46189  fourierdlem87  46191  fourierdlem88  46192  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  elaa2lem  46231  etransclem4  46236  etransclem13  46245  etransclem35  46267  etransclem46  46278  etransclem48  46280  sge0revalmpt  46376  sge0fsummpt  46388  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0ltfirpmpt2  46424  sge0fsummptf  46434  nnfoctbdjlem  46453  iundjiun  46458  meaiunlelem  46466  meaiuninclem  46478  meaiuninc3v  46482  omeiunlempt  46518  carageniuncllem2  46520  caratheodorylem2  46525  0ome  46527  isomenndlem  46528  hoicvr  46546  hoicvrrex  46554  ovn0lem  46563  ovnsubaddlem1  46568  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem2  46600  hoicoto2  46603  hoi2toco  46605  ovnlecvr2  46608  ovncvr2  46609  ovnsubadd2lem  46643  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  vonioolem1  46678  smfaddlem1  46761  smflimlem2  46770  smflimmpt  46808  smflimsuplem2  46819  smflimsuplem4  46821  smflimsuplem5  46822  smflimsupmpt  46827  smfliminfmpt  46830  smfsupdmmbllem  46842  finfdm  46844  smfinfdmmbllem  46846  setrec2mpt  49686  aacllem  49790