Theorem fvmpt2 6997

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186   I cid 5545  ‘cfv 6531

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fv 6539

This theorem is used by:  fvmptss  6998  fvmpt2d  6999  fvmptd3f  7001  mpteqb  7005  fvmptt  7006  fvmptf  7007  fnmptfvd  7032  ralrnmptw  7086  ralrnmpt  7088  fompt  7110  fmptco  7122  f1mpt  7257  offval2  7702  ofrfval2  7703  fimaproj  8136  mptelixpg  8947  dom2lem  9003  mapxpen  9146  xpmapenlem  9147  cnfcom3clem  9690  tcvalg  9721  rankf  9784  infxpenc2lem2  10080  dfac8clem  10092  acni2  10106  acnlem  10108  fin23lem32  10403  axcc2lem  10495  axcc3  10497  domtriomlem  10501  ac6num  10538  konigthlem  10634  rpnnen1lem1  13087  rpnnen1lem3  13088  rpnnen1lem5  13090  seqof  14182  seqof2  14183  rlim2  15643  ello1mpt  15668  o1compt  15734  sumrblem  15857  fsumcvg  15858  summolem2a  15861  fsum  15866  fsumcvg2  15873  fsumadd  15886  isummulc2  15908  fsummulc2  15930  fsumrelem  15954  prodrblem  16076  fprodcvg  16077  prodmolem2a  16081  zprod  16084  fprod  16088  fprodmul  16107  fproddiv  16108  iserodd  16993  prmrec  17080  prdsbas3  17632  prdsdsval2  17635  invfuc  18132  yonedalem4c  18431  smndex1n0mnd  19091  gsumconst  20128  prdsgsum  20175  gsumdixp  20528  pwsgprod  20539  evlslem4  22365  matunitlindflem2  22975  elptr2  23873  ptunimpt  23894  ptcldmpt  23913  ptclsg  23914  txcnp  23919  ptcnplem  23920  cnmpt11  23962  cnmpt1t  23964  cnmptk2  23985  xkocnv  24113  flfcnp2  24306  ustn0  24520  utopsnneiplem  24546  ucnima  24579  iccpnfcnv  25245  ovolctb  25791  ovoliunlem1  25803  ovoliun2  25807  ovolshftlem1  25810  ovolscalem1  25814  voliun  25855  ioombl1lem3  25861  ioombl1lem4  25862  uniioombllem2  25884  mbfeqalem1  25942  mbfpos  25952  mbfposr  25953  mbfposb  25954  mbfsup  25965  mbfinf  25966  mbflim  25969  i1fposd  26008  itg1climres  26015  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mbfi1fseqlem6  26021  itg2split  26050  itg2mono  26054  itg2cnlem1  26062  isibl2  26067  itgmpt  26083  itgeqa  26114  itggt0  26144  itgcn  26145  limcmpt  26183  dvlipcn  26294  lhop2  26315  dvfsumabs  26323  itgparts  26347  itgsubstlem  26348  itgsubst  26349  elplyd  26500  coeeulem  26523  coeeq2  26541  dvply1  26587  plyremlem  26607  ulmss  26706  ulmdvlem1  26709  mtest  26713  itgulm2  26718  radcnvlem1  26722  pserulm  26731  leibpi  27252  rlimcnp  27275  o1cxp  27284  lgamgulmlem2  27339  lgamgulmlem6  27343  lgamgulm2  27345  sqff1o  27491  lgseisenlem2  27685  dchrvmasumlem1  27804  frgrncvvdeqlem5  30886  ubthlem1  31454  cnlnadjlem5  32655  xppreima2  33227  abfmpunirn  33228  aciunf1lem  33238  suppovss  33256  fpwrelmap  33307  suppgsumssiun  33615  nsgmgc  33945  zringfrac  34068  extdgfialglem2  34307  algextdeglem6  34336  xrmulc1cn  34544  esumpcvgval  34692  esumsup  34703  voliune  34844  eulerpartgbij  34987  signsplypnf  35162  wevgblacfn  35863  iscvm  35993  mclsrcl  36295  f1omptsnlem  38227  itg2addnclem  38557  itggt0cn  38576  ftc1anclem5  38583  elrfirn2  43660  eq0rabdioph  43740  monotoddzz  43903  aomclem2  44015  refsumcn  45990  refsum2cnlem1  45997  fvmpt2bd  46128  choicefi  46157  axccdom  46178  fvmpt4  46193  fsumsermpt  46535  fmuldfeqlem1  46538  fmuldfeq  46539  climneg  46566  climdivf  46568  mullimc  46572  idlimc  46582  sumnnodd  46586  neglimc  46601  addlimc  46602  0ellimcdiv  46603  climfveqmpt2  46647  climeqmpt  46651  limsupequzmptlem  46682  liminfvalxr  46737  xlimmnfmpt  46797  xlimpnfmpt  46798  cncfmptssg  46825  cncfshift  46828  icccncfext  46841  cncfiooicclem1  46847  fprodsubrecnncnvlem  46861  fprodaddrecnncnvlem  46863  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvnmptdivc  46892  dvnmul  46897  dvnprodlem2  46901  itgsin0pilem1  46904  ibliccsinexp  46905  itgsinexplem1  46908  itgsinexp  46909  ditgeqiooicc  46914  itgsubsticclem  46929  itgioocnicc  46931  stoweidlem2  46956  stoweidlem11  46965  stoweidlem12  46966  stoweidlem16  46970  stoweidlem17  46971  stoweidlem18  46972  stoweidlem19  46973  stoweidlem20  46974  stoweidlem21  46975  stoweidlem22  46976  stoweidlem23  46977  stoweidlem27  46981  stoweidlem31  46985  stoweidlem34  46988  stoweidlem36  46990  stoweidlem40  46994  stoweidlem41  46995  stoweidlem42  46996  stoweidlem48  47002  stoweidlem55  47009  stoweidlem59  47013  stoweidlem62  47016  stirlinglem3  47030  stirlinglem8  47035  stirlinglem14  47041  stirlinglem15  47042  stirlingr  47044  dirkeritg  47056  dirkercncflem2  47058  fourierdlem14  47075  fourierdlem31  47092  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem56  47116  fourierdlem60  47120  fourierdlem61  47121  fourierdlem66  47126  fourierdlem70  47130  fourierdlem71  47131  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem77  47137  fourierdlem78  47138  fourierdlem81  47141  fourierdlem83  47143  fourierdlem84  47144  fourierdlem85  47145  fourierdlem87  47147  fourierdlem88  47148  fourierdlem89  47149  fourierdlem91  47151  fourierdlem92  47152  fourierdlem93  47153  fourierdlem95  47155  fourierdlem97  47157  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  sqwvfoura  47182  sqwvfourb  47183  fouriersw  47185  elaa2lem  47187  etransclem4  47192  etransclem13  47201  etransclem35  47223  etransclem46  47234  etransclem48  47236  sge0revalmpt  47332  sge0fsummpt  47344  sge0iunmptlemfi  47367  sge0iunmptlemre  47369  sge0ltfirpmpt2  47380  sge0fsummptf  47390  nnfoctbdjlem  47409  iundjiun  47414  meaiunlelem  47422  meaiuninclem  47434  meaiuninc3v  47438  omeiunlempt  47474  carageniuncllem2  47476  caratheodorylem2  47481  0ome  47483  isomenndlem  47484  hoicvr  47502  hoicvrrex  47510  ovn0lem  47519  ovnsubaddlem1  47524  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoilem2  47556  hoicoto2  47559  hoi2toco  47561  ovnlecvr2  47564  ovncvr2  47565  ovnsubadd2lem  47599  ovolval5lem2  47607  ovnovollem1  47610  ovnovollem2  47611  vonioolem1  47634  smfaddlem1  47717  smflimlem2  47726  smflimmpt  47764  smflimsuplem2  47775  smflimsuplem4  47777  smflimsuplem5  47778  smflimsupmpt  47783  smfliminfmpt  47786  smfsupdmmbllem  47798  finfdm  47800  smfinfdmmbllem  47802  setrec2mpt  50734  aacllem  50883