Theorem fvmpt2 6953

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5167   I cid 5518  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptss  6954  fvmpt2d  6955  fvmptd3f  6957  mpteqb  6961  fvmptt  6962  fvmptf  6963  fnmptfvd  6987  ralrnmptw  7040  ralrnmpt  7042  fompt  7064  fmptco  7076  f1mpt  7209  offval2  7644  ofrfval2  7645  fimaproj  8078  mptelixpg  8876  dom2lem  8932  mapxpen  9074  xpmapenlem  9075  cnfcom3clem  9617  tcvalg  9648  rankf  9709  infxpenc2lem2  9933  dfac8clem  9945  acni2  9959  acnlem  9961  fin23lem32  10257  axcc2lem  10349  axcc3  10351  domtriomlem  10355  ac6num  10392  konigthlem  10482  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  seqof  14012  seqof2  14013  rlim2  15449  ello1mpt  15474  o1compt  15540  sumrblem  15664  fsumcvg  15665  summolem2a  15668  fsum  15673  fsumcvg2  15680  fsumadd  15693  isummulc2  15715  fsummulc2  15737  fsumrelem  15761  prodrblem  15885  fprodcvg  15886  prodmolem2a  15890  zprod  15893  fprod  15897  fprodmul  15916  fproddiv  15917  iserodd  16797  prmrec  16884  prdsbas3  17435  prdsdsval2  17438  invfuc  17935  yonedalem4c  18234  smndex1n0mnd  18874  gsumconst  19900  prdsgsum  19947  gsumdixp  20289  pwsgprod  20300  evlslem4  22064  elptr2  23549  ptunimpt  23570  ptcldmpt  23589  ptclsg  23590  txcnp  23595  ptcnplem  23596  cnmpt11  23638  cnmpt1t  23640  cnmptk2  23661  xkocnv  23789  flfcnp2  23982  ustn0  24196  utopsnneiplem  24222  ucnima  24255  iccpnfcnv  24921  ovolctb  25467  ovoliunlem1  25479  ovoliun2  25483  ovolshftlem1  25486  ovolscalem1  25490  voliun  25531  ioombl1lem3  25537  ioombl1lem4  25538  uniioombllem2  25560  mbfeqalem1  25618  mbfpos  25628  mbfposr  25629  mbfposb  25630  mbfsup  25641  mbfinf  25642  mbflim  25645  i1fposd  25684  itg1climres  25691  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2split  25726  itg2mono  25730  itg2cnlem1  25738  isibl2  25743  itgmpt  25760  itgeqa  25791  itggt0  25821  itgcn  25822  limcmpt  25860  dvlipcn  25971  lhop2  25992  dvfsumabs  26000  itgparts  26024  itgsubstlem  26025  itgsubst  26026  elplyd  26177  coeeulem  26199  coeeq2  26217  dvply1  26260  plyremlem  26281  ulmss  26375  ulmdvlem1  26378  mtest  26382  itgulm2  26387  radcnvlem1  26391  pserulm  26400  leibpi  26919  rlimcnp  26942  o1cxp  26952  lgamgulmlem2  27007  lgamgulmlem6  27011  lgamgulm2  27013  sqff1o  27159  lgseisenlem2  27353  dchrvmasumlem1  27472  frgrncvvdeqlem5  30388  ubthlem1  30956  cnlnadjlem5  32157  xppreima2  32739  abfmpunirn  32740  aciunf1lem  32750  suppovss  32769  fpwrelmap  32821  suppgsumssiun  33148  nsgmgc  33487  zringfrac  33629  extdgfialglem2  33853  algextdeglem6  33882  xrmulc1cn  34090  esumpcvgval  34238  esumsup  34249  voliune  34389  eulerpartgbij  34532  signsplypnf  34710  wevgblacfn  35307  iscvm  35457  mclsrcl  35759  f1omptsnlem  37666  matunitlindflem2  37952  itg2addnclem  38006  itggt0cn  38025  ftc1anclem5  38032  elrfirn2  43142  eq0rabdioph  43222  monotoddzz  43389  aomclem2  43501  refsumcn  45479  refsum2cnlem1  45486  fvmpt2bd  45618  choicefi  45647  axccdom  45669  fvmpt4  45685  fsumsermpt  46027  fmuldfeqlem1  46030  fmuldfeq  46031  climneg  46058  climdivf  46060  mullimc  46064  idlimc  46074  sumnnodd  46078  neglimc  46093  addlimc  46094  0ellimcdiv  46095  climfveqmpt2  46139  climeqmpt  46143  limsupequzmptlem  46174  liminfvalxr  46229  xlimmnfmpt  46289  xlimpnfmpt  46290  cncfmptssg  46317  cncfshift  46320  icccncfext  46333  cncfiooicclem1  46339  fprodsubrecnncnvlem  46353  fprodaddrecnncnvlem  46355  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnmptdivc  46384  dvnmul  46389  dvnprodlem2  46393  itgsin0pilem1  46396  ibliccsinexp  46397  itgsinexplem1  46400  itgsinexp  46401  ditgeqiooicc  46406  itgsubsticclem  46421  itgioocnicc  46423  stoweidlem2  46448  stoweidlem11  46457  stoweidlem12  46458  stoweidlem16  46462  stoweidlem17  46463  stoweidlem18  46464  stoweidlem19  46465  stoweidlem20  46466  stoweidlem21  46467  stoweidlem22  46468  stoweidlem23  46469  stoweidlem27  46473  stoweidlem31  46477  stoweidlem34  46480  stoweidlem36  46482  stoweidlem40  46486  stoweidlem41  46487  stoweidlem42  46488  stoweidlem48  46494  stoweidlem55  46501  stoweidlem59  46505  stoweidlem62  46508  stirlinglem3  46522  stirlinglem8  46527  stirlinglem14  46533  stirlinglem15  46534  stirlingr  46536  dirkeritg  46548  dirkercncflem2  46550  fourierdlem14  46567  fourierdlem31  46584  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem56  46608  fourierdlem60  46612  fourierdlem61  46613  fourierdlem66  46618  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem77  46629  fourierdlem78  46630  fourierdlem81  46633  fourierdlem83  46635  fourierdlem84  46636  fourierdlem85  46637  fourierdlem87  46639  fourierdlem88  46640  fourierdlem89  46641  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem95  46647  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  elaa2lem  46679  etransclem4  46684  etransclem13  46693  etransclem35  46715  etransclem46  46726  etransclem48  46728  sge0revalmpt  46824  sge0fsummpt  46836  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0ltfirpmpt2  46872  sge0fsummptf  46882  nnfoctbdjlem  46901  iundjiun  46906  meaiunlelem  46914  meaiuninclem  46926  meaiuninc3v  46930  omeiunlempt  46966  carageniuncllem2  46968  caratheodorylem2  46973  0ome  46975  isomenndlem  46976  hoicvr  46994  hoicvrrex  47002  ovn0lem  47011  ovnsubaddlem1  47016  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem2  47048  hoicoto2  47051  hoi2toco  47053  ovnlecvr2  47056  ovncvr2  47057  ovnsubadd2lem  47091  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  vonioolem1  47126  smfaddlem1  47209  smflimlem2  47218  smflimmpt  47256  smflimsuplem2  47267  smflimsuplem4  47269  smflimsuplem5  47270  smflimsupmpt  47275  smfliminfmpt  47278  smfsupdmmbllem  47290  finfdm  47292  smfinfdmmbllem  47294  setrec2mpt  50184  aacllem  50288