Theorem fvmpt2 7002

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

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

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  fvmptss  7003  fvmpt2d  7004  fvmptd3f  7006  mpteqb  7010  fvmptt  7011  fvmptf  7012  fnmptfvd  7037  ralrnmptw  7091  ralrnmpt  7093  fompt  7115  fmptco  7127  f1mpt  7262  offval2  7702  ofrfval2  7703  fimaproj  8137  mptelixpg  8946  dom2lem  9002  mapxpen  9145  xpmapenlem  9146  cnfcom3clem  9688  tcvalg  9719  rankf  9780  infxpenc2lem2  10027  dfac8clem  10039  acni2  10053  acnlem  10055  fin23lem32  10350  axcc2lem  10442  axcc3  10444  domtriomlem  10448  ac6num  10485  konigthlem  10581  rpnnen1lem1  13032  rpnnen1lem3  13033  rpnnen1lem5  13035  seqof  14127  seqof2  14128  rlim2  15587  ello1mpt  15612  o1compt  15678  sumrblem  15801  fsumcvg  15802  summolem2a  15805  fsum  15810  fsumcvg2  15817  fsumadd  15830  isummulc2  15852  fsummulc2  15874  fsumrelem  15898  prodrblem  16022  fprodcvg  16023  prodmolem2a  16027  zprod  16030  fprod  16034  fprodmul  16053  fproddiv  16054  iserodd  16933  prmrec  17020  prdsbas3  17572  prdsdsval2  17575  invfuc  18072  yonedalem4c  18371  smndex1n0mnd  19030  gsumconst  20067  prdsgsum  20114  gsumdixp  20465  pwsgprod  20476  evlslem4  22298  matunitlindflem2  22908  elptr2  23806  ptunimpt  23827  ptcldmpt  23846  ptclsg  23847  txcnp  23852  ptcnplem  23853  cnmpt11  23895  cnmpt1t  23897  cnmptk2  23918  xkocnv  24046  flfcnp2  24239  ustn0  24453  utopsnneiplem  24479  ucnima  24512  iccpnfcnv  25178  ovolctb  25724  ovoliunlem1  25736  ovoliun2  25740  ovolshftlem1  25743  ovolscalem1  25747  voliun  25788  ioombl1lem3  25794  ioombl1lem4  25795  uniioombllem2  25817  mbfeqalem1  25875  mbfpos  25885  mbfposr  25886  mbfposb  25887  mbfsup  25898  mbfinf  25899  mbflim  25902  i1fposd  25941  itg1climres  25948  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1fseqlem6  25954  itg2split  25983  itg2mono  25987  itg2cnlem1  25995  isibl2  26000  itgmpt  26017  itgeqa  26048  itggt0  26078  itgcn  26079  limcmpt  26117  dvlipcn  26228  lhop2  26249  dvfsumabs  26257  itgparts  26281  itgsubstlem  26282  itgsubst  26283  elplyd  26434  coeeulem  26457  coeeq2  26475  dvply1  26521  plyremlem  26541  ulmss  26640  ulmdvlem1  26643  mtest  26647  itgulm2  26652  radcnvlem1  26656  pserulm  26665  leibpi  27187  rlimcnp  27210  o1cxp  27219  lgamgulmlem2  27274  lgamgulmlem6  27278  lgamgulm2  27280  sqff1o  27426  lgseisenlem2  27620  dchrvmasumlem1  27739  frgrncvvdeqlem5  30791  ubthlem1  31359  cnlnadjlem5  32560  xppreima2  33132  abfmpunirn  33133  aciunf1lem  33143  suppovss  33161  fpwrelmap  33212  suppgsumssiun  33520  nsgmgc  33849  zringfrac  33972  extdgfialglem2  34211  algextdeglem6  34240  xrmulc1cn  34448  esumpcvgval  34596  esumsup  34607  voliune  34748  eulerpartgbij  34891  signsplypnf  35066  wevgblacfn  35716  iscvm  35846  mclsrcl  36148  f1omptsnlem  38098  itg2addnclem  38428  itggt0cn  38447  ftc1anclem5  38454  elrfirn2  43549  eq0rabdioph  43629  monotoddzz  43792  aomclem2  43904  refsumcn  45872  refsum2cnlem1  45879  fvmpt2bd  46010  choicefi  46039  axccdom  46060  fvmpt4  46075  fsumsermpt  46417  fmuldfeqlem1  46420  fmuldfeq  46421  climneg  46448  climdivf  46450  mullimc  46454  idlimc  46464  sumnnodd  46468  neglimc  46483  addlimc  46484  0ellimcdiv  46485  climfveqmpt2  46529  climeqmpt  46533  limsupequzmptlem  46564  liminfvalxr  46619  xlimmnfmpt  46679  xlimpnfmpt  46680  cncfmptssg  46707  cncfshift  46710  icccncfext  46723  cncfiooicclem1  46729  fprodsubrecnncnvlem  46743  fprodaddrecnncnvlem  46745  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnmptdivc  46774  dvnmul  46779  dvnprodlem2  46783  itgsin0pilem1  46786  ibliccsinexp  46787  itgsinexplem1  46790  itgsinexp  46791  ditgeqiooicc  46796  itgsubsticclem  46811  itgioocnicc  46813  stoweidlem2  46838  stoweidlem11  46847  stoweidlem12  46848  stoweidlem16  46852  stoweidlem17  46853  stoweidlem18  46854  stoweidlem19  46855  stoweidlem20  46856  stoweidlem21  46857  stoweidlem22  46858  stoweidlem23  46859  stoweidlem27  46863  stoweidlem31  46867  stoweidlem34  46870  stoweidlem36  46872  stoweidlem40  46876  stoweidlem41  46877  stoweidlem42  46878  stoweidlem48  46884  stoweidlem55  46891  stoweidlem59  46895  stoweidlem62  46898  stirlinglem3  46912  stirlinglem8  46917  stirlinglem14  46923  stirlinglem15  46924  stirlingr  46926  dirkeritg  46938  dirkercncflem2  46940  fourierdlem14  46957  fourierdlem31  46974  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem56  46998  fourierdlem60  47002  fourierdlem61  47003  fourierdlem66  47008  fourierdlem70  47012  fourierdlem71  47013  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem77  47019  fourierdlem78  47020  fourierdlem81  47023  fourierdlem83  47025  fourierdlem84  47026  fourierdlem85  47027  fourierdlem87  47029  fourierdlem88  47030  fourierdlem89  47031  fourierdlem91  47033  fourierdlem92  47034  fourierdlem93  47035  fourierdlem95  47037  fourierdlem97  47039  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  elaa2lem  47069  etransclem4  47074  etransclem13  47083  etransclem35  47105  etransclem46  47116  etransclem48  47118  sge0revalmpt  47214  sge0fsummpt  47226  sge0iunmptlemfi  47249  sge0iunmptlemre  47251  sge0ltfirpmpt2  47262  sge0fsummptf  47272  nnfoctbdjlem  47291  iundjiun  47296  meaiunlelem  47304  meaiuninclem  47316  meaiuninc3v  47320  omeiunlempt  47356  carageniuncllem2  47358  caratheodorylem2  47363  0ome  47365  isomenndlem  47366  hoicvr  47384  hoicvrrex  47392  ovn0lem  47401  ovnsubaddlem1  47406  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoilem2  47438  hoicoto2  47441  hoi2toco  47443  ovnlecvr2  47446  ovncvr2  47447  ovnsubadd2lem  47481  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493  vonioolem1  47516  smfaddlem1  47599  smflimlem2  47608  smflimmpt  47646  smflimsuplem2  47657  smflimsuplem4  47659  smflimsuplem5  47660  smflimsupmpt  47665  smfliminfmpt  47668  smfsupdmmbllem  47680  finfdm  47682  smfinfdmmbllem  47684  setrec2mpt  50631  aacllem  50780