Theorem fvmpt2 6991

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5186   I cid 5546  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  fvmptss  6992  fvmpt2d  6993  fvmptd3f  6995  mpteqb  6999  fvmptt  7000  fvmptf  7001  fnmptfvd  7026  ralrnmptw  7079  ralrnmpt  7081  fompt  7103  fmptco  7115  f1mpt  7249  offval2  7684  ofrfval2  7685  fimaproj  8119  mptelixpg  8921  dom2lem  8977  mapxpen  9119  xpmapenlem  9120  cnfcom3clem  9662  tcvalg  9693  rankf  9754  infxpenc2lem2  9992  dfac8clem  10004  acni2  10018  acnlem  10020  fin23lem32  10316  axcc2lem  10408  axcc3  10410  domtriomlem  10414  ac6num  10451  konigthlem  10541  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem5  12996  seqof  14086  seqof2  14087  rlim2  15537  ello1mpt  15562  o1compt  15628  sumrblem  15752  fsumcvg  15753  summolem2a  15756  fsum  15761  fsumcvg2  15768  fsumadd  15781  isummulc2  15803  fsummulc2  15825  fsumrelem  15849  prodrblem  15973  fprodcvg  15974  prodmolem2a  15978  zprod  15981  fprod  15985  fprodmul  16004  fproddiv  16005  iserodd  16885  prmrec  16972  prdsbas3  17524  prdsdsval2  17527  invfuc  18024  yonedalem4c  18323  smndex1n0mnd  18964  gsumconst  19995  prdsgsum  20042  gsumdixp  20391  pwsgprod  20402  evlslem4  22187  elptr2  23692  ptunimpt  23713  ptcldmpt  23732  ptclsg  23733  txcnp  23738  ptcnplem  23739  cnmpt11  23781  cnmpt1t  23783  cnmptk2  23804  xkocnv  23932  flfcnp2  24125  ustn0  24339  utopsnneiplem  24365  ucnima  24398  iccpnfcnv  25064  ovolctb  25610  ovoliunlem1  25622  ovoliun2  25626  ovolshftlem1  25629  ovolscalem1  25633  voliun  25674  ioombl1lem3  25680  ioombl1lem4  25681  uniioombllem2  25703  mbfeqalem1  25761  mbfpos  25771  mbfposr  25772  mbfposb  25773  mbfsup  25784  mbfinf  25785  mbflim  25788  i1fposd  25827  itg1climres  25834  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1fseqlem6  25840  itg2split  25869  itg2mono  25873  itg2cnlem1  25881  isibl2  25886  itgmpt  25903  itgeqa  25934  itggt0  25964  itgcn  25965  limcmpt  26003  dvlipcn  26114  lhop2  26135  dvfsumabs  26143  itgparts  26167  itgsubstlem  26168  itgsubst  26169  elplyd  26320  coeeulem  26342  coeeq2  26360  dvply1  26406  plyremlem  26426  ulmss  26518  ulmdvlem1  26521  mtest  26525  itgulm2  26530  radcnvlem1  26534  pserulm  26543  leibpi  27065  rlimcnp  27088  o1cxp  27097  lgamgulmlem2  27152  lgamgulmlem6  27156  lgamgulm2  27158  sqff1o  27304  lgseisenlem2  27498  dchrvmasumlem1  27617  frgrncvvdeqlem5  30563  ubthlem1  31131  cnlnadjlem5  32332  xppreima2  32908  abfmpunirn  32909  aciunf1lem  32919  suppovss  32938  fpwrelmap  32990  suppgsumssiun  33305  nsgmgc  33637  zringfrac  33761  extdgfialglem2  34000  algextdeglem6  34029  xrmulc1cn  34237  esumpcvgval  34385  esumsup  34396  voliune  34536  eulerpartgbij  34679  signsplypnf  34854  wevgblacfn  35466  iscvm  35622  mclsrcl  35924  f1omptsnlem  37842  matunitlindflem2  38128  itg2addnclem  38182  itggt0cn  38201  ftc1anclem5  38208  elrfirn2  43289  eq0rabdioph  43369  monotoddzz  43532  aomclem2  43644  refsumcn  45608  refsum2cnlem1  45615  fvmpt2bd  45746  choicefi  45775  axccdom  45796  fvmpt4  45811  fsumsermpt  46153  fmuldfeqlem1  46156  fmuldfeq  46157  climneg  46184  climdivf  46186  mullimc  46190  idlimc  46200  sumnnodd  46204  neglimc  46219  addlimc  46220  0ellimcdiv  46221  climfveqmpt2  46265  climeqmpt  46269  limsupequzmptlem  46300  liminfvalxr  46355  xlimmnfmpt  46415  xlimpnfmpt  46416  cncfmptssg  46443  cncfshift  46446  icccncfext  46459  cncfiooicclem1  46465  fprodsubrecnncnvlem  46479  fprodaddrecnncnvlem  46481  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvnmptdivc  46510  dvnmul  46515  dvnprodlem2  46519  itgsin0pilem1  46522  ibliccsinexp  46523  itgsinexplem1  46526  itgsinexp  46527  ditgeqiooicc  46532  itgsubsticclem  46547  itgioocnicc  46549  stoweidlem2  46574  stoweidlem11  46583  stoweidlem12  46584  stoweidlem16  46588  stoweidlem17  46589  stoweidlem18  46590  stoweidlem19  46591  stoweidlem20  46592  stoweidlem21  46593  stoweidlem22  46594  stoweidlem23  46595  stoweidlem27  46599  stoweidlem31  46603  stoweidlem34  46606  stoweidlem36  46608  stoweidlem40  46612  stoweidlem41  46613  stoweidlem42  46614  stoweidlem48  46620  stoweidlem55  46627  stoweidlem59  46631  stoweidlem62  46634  stirlinglem3  46648  stirlinglem8  46653  stirlinglem14  46659  stirlinglem15  46660  stirlingr  46662  dirkeritg  46674  dirkercncflem2  46676  fourierdlem14  46693  fourierdlem31  46710  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem51  46729  fourierdlem56  46734  fourierdlem60  46738  fourierdlem61  46739  fourierdlem66  46744  fourierdlem70  46748  fourierdlem71  46749  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem77  46755  fourierdlem78  46756  fourierdlem81  46759  fourierdlem83  46761  fourierdlem84  46762  fourierdlem85  46763  fourierdlem87  46765  fourierdlem88  46766  fourierdlem89  46767  fourierdlem91  46769  fourierdlem92  46770  fourierdlem93  46771  fourierdlem95  46773  fourierdlem97  46775  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem112  46790  sqwvfoura  46800  sqwvfourb  46801  fouriersw  46803  elaa2lem  46805  etransclem4  46810  etransclem13  46819  etransclem35  46841  etransclem46  46852  etransclem48  46854  sge0revalmpt  46950  sge0fsummpt  46962  sge0iunmptlemfi  46985  sge0iunmptlemre  46987  sge0ltfirpmpt2  46998  sge0fsummptf  47008  nnfoctbdjlem  47027  iundjiun  47032  meaiunlelem  47040  meaiuninclem  47052  meaiuninc3v  47056  omeiunlempt  47092  carageniuncllem2  47094  caratheodorylem2  47099  0ome  47101  isomenndlem  47102  hoicvr  47120  hoicvrrex  47128  ovn0lem  47137  ovnsubaddlem1  47142  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoilem2  47174  hoicoto2  47177  hoi2toco  47179  ovnlecvr2  47182  ovncvr2  47183  ovnsubadd2lem  47217  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  vonioolem1  47252  smfaddlem1  47335  smflimlem2  47344  smflimmpt  47382  smflimsuplem2  47393  smflimsuplem4  47395  smflimsuplem5  47396  smflimsupmpt  47401  smfliminfmpt  47404  smfsupdmmbllem  47416  finfdm  47418  smfinfdmmbllem  47420  setrec2mpt  50326  aacllem  50430