Theorem fvmpt2 7003

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193   I cid 5557  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  fvmptss  7004  fvmpt2d  7005  fvmptd3f  7007  mpteqb  7011  fvmptt  7012  fvmptf  7013  fnmptfvd  7038  ralrnmptw  7091  ralrnmpt  7093  fompt  7115  fmptco  7127  f1mpt  7261  offval2  7696  ofrfval2  7697  fimaproj  8132  mptelixpg  8934  dom2lem  8990  mapxpen  9132  xpmapenlem  9133  cnfcom3clem  9675  tcvalg  9706  rankf  9767  infxpenc2lem2  10005  dfac8clem  10017  acni2  10031  acnlem  10033  fin23lem32  10329  axcc2lem  10421  axcc3  10423  domtriomlem  10427  ac6num  10464  konigthlem  10554  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  seqof  14097  seqof2  14098  rlim2  15549  ello1mpt  15574  o1compt  15640  sumrblem  15764  fsumcvg  15765  summolem2a  15768  fsum  15773  fsumcvg2  15780  fsumadd  15793  isummulc2  15815  fsummulc2  15837  fsumrelem  15861  prodrblem  15985  fprodcvg  15986  prodmolem2a  15990  zprod  15993  fprod  15997  fprodmul  16016  fproddiv  16017  iserodd  16896  prmrec  16983  prdsbas3  17535  prdsdsval2  17538  invfuc  18035  yonedalem4c  18334  smndex1n0mnd  18975  gsumconst  20005  prdsgsum  20052  gsumdixp  20401  pwsgprod  20412  evlslem4  22208  elptr2  23712  ptunimpt  23733  ptcldmpt  23752  ptclsg  23753  txcnp  23758  ptcnplem  23759  cnmpt11  23801  cnmpt1t  23803  cnmptk2  23824  xkocnv  23952  flfcnp2  24145  ustn0  24359  utopsnneiplem  24385  ucnima  24418  iccpnfcnv  25084  ovolctb  25630  ovoliunlem1  25642  ovoliun2  25646  ovolshftlem1  25649  ovolscalem1  25653  voliun  25694  ioombl1lem3  25700  ioombl1lem4  25701  uniioombllem2  25723  mbfeqalem1  25781  mbfpos  25791  mbfposr  25792  mbfposb  25793  mbfsup  25804  mbfinf  25805  mbflim  25808  i1fposd  25847  itg1climres  25854  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  itg2split  25889  itg2mono  25893  itg2cnlem1  25901  isibl2  25906  itgmpt  25923  itgeqa  25954  itggt0  25984  itgcn  25985  limcmpt  26023  dvlipcn  26134  lhop2  26155  dvfsumabs  26163  itgparts  26187  itgsubstlem  26188  itgsubst  26189  elplyd  26340  coeeulem  26362  coeeq2  26380  dvply1  26426  plyremlem  26446  ulmss  26538  ulmdvlem1  26541  mtest  26545  itgulm2  26550  radcnvlem1  26554  pserulm  26563  leibpi  27085  rlimcnp  27108  o1cxp  27117  lgamgulmlem2  27172  lgamgulmlem6  27176  lgamgulm2  27178  sqff1o  27324  lgseisenlem2  27518  dchrvmasumlem1  27637  frgrncvvdeqlem5  30632  ubthlem1  31200  cnlnadjlem5  32401  xppreima2  32974  abfmpunirn  32975  aciunf1lem  32985  suppovss  33004  fpwrelmap  33056  suppgsumssiun  33370  nsgmgc  33699  zringfrac  33822  extdgfialglem2  34061  algextdeglem6  34090  xrmulc1cn  34298  esumpcvgval  34446  esumsup  34457  voliune  34597  eulerpartgbij  34740  signsplypnf  34915  wevgblacfn  35573  iscvm  35729  mclsrcl  36031  f1omptsnlem  37960  matunitlindflem2  38246  itg2addnclem  38300  itggt0cn  38319  ftc1anclem5  38326  elrfirn2  43407  eq0rabdioph  43487  monotoddzz  43650  aomclem2  43762  refsumcn  45730  refsum2cnlem1  45737  fvmpt2bd  45868  choicefi  45897  axccdom  45918  fvmpt4  45933  fsumsermpt  46275  fmuldfeqlem1  46278  fmuldfeq  46279  climneg  46306  climdivf  46308  mullimc  46312  idlimc  46322  sumnnodd  46326  neglimc  46341  addlimc  46342  0ellimcdiv  46343  climfveqmpt2  46387  climeqmpt  46391  limsupequzmptlem  46422  liminfvalxr  46477  xlimmnfmpt  46537  xlimpnfmpt  46538  cncfmptssg  46565  cncfshift  46568  icccncfext  46581  cncfiooicclem1  46587  fprodsubrecnncnvlem  46601  fprodaddrecnncnvlem  46603  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvnmptdivc  46632  dvnmul  46637  dvnprodlem2  46641  itgsin0pilem1  46644  ibliccsinexp  46645  itgsinexplem1  46648  itgsinexp  46649  ditgeqiooicc  46654  itgsubsticclem  46669  itgioocnicc  46671  stoweidlem2  46696  stoweidlem11  46705  stoweidlem12  46706  stoweidlem16  46710  stoweidlem17  46711  stoweidlem18  46712  stoweidlem19  46713  stoweidlem20  46714  stoweidlem21  46715  stoweidlem22  46716  stoweidlem23  46717  stoweidlem27  46721  stoweidlem31  46725  stoweidlem34  46728  stoweidlem36  46730  stoweidlem40  46734  stoweidlem41  46735  stoweidlem42  46736  stoweidlem48  46742  stoweidlem55  46749  stoweidlem59  46753  stoweidlem62  46756  stirlinglem3  46770  stirlinglem8  46775  stirlinglem14  46781  stirlinglem15  46782  stirlingr  46784  dirkeritg  46796  dirkercncflem2  46798  fourierdlem14  46815  fourierdlem31  46832  fourierdlem41  46842  fourierdlem48  46848  fourierdlem49  46849  fourierdlem50  46850  fourierdlem51  46851  fourierdlem56  46856  fourierdlem60  46860  fourierdlem61  46861  fourierdlem66  46866  fourierdlem70  46870  fourierdlem71  46871  fourierdlem73  46873  fourierdlem74  46874  fourierdlem75  46875  fourierdlem76  46876  fourierdlem77  46877  fourierdlem78  46878  fourierdlem81  46881  fourierdlem83  46883  fourierdlem84  46884  fourierdlem85  46885  fourierdlem87  46887  fourierdlem88  46888  fourierdlem89  46889  fourierdlem91  46891  fourierdlem92  46892  fourierdlem93  46893  fourierdlem95  46895  fourierdlem97  46897  fourierdlem101  46901  fourierdlem103  46903  fourierdlem104  46904  fourierdlem111  46911  fourierdlem112  46912  sqwvfoura  46922  sqwvfourb  46923  fouriersw  46925  elaa2lem  46927  etransclem4  46932  etransclem13  46941  etransclem35  46963  etransclem46  46974  etransclem48  46976  sge0revalmpt  47072  sge0fsummpt  47084  sge0iunmptlemfi  47107  sge0iunmptlemre  47109  sge0ltfirpmpt2  47120  sge0fsummptf  47130  nnfoctbdjlem  47149  iundjiun  47154  meaiunlelem  47162  meaiuninclem  47174  meaiuninc3v  47178  omeiunlempt  47214  carageniuncllem2  47216  caratheodorylem2  47221  0ome  47223  isomenndlem  47224  hoicvr  47242  hoicvrrex  47250  ovn0lem  47259  ovnsubaddlem1  47264  hoidmvlelem2  47290  hoidmvlelem3  47291  ovnhoilem2  47296  hoicoto2  47299  hoi2toco  47301  ovnlecvr2  47304  ovncvr2  47305  ovnsubadd2lem  47339  ovolval5lem2  47347  ovnovollem1  47350  ovnovollem2  47351  vonioolem1  47374  smfaddlem1  47457  smflimlem2  47466  smflimmpt  47504  smflimsuplem2  47515  smflimsuplem4  47517  smflimsuplem5  47518  smflimsupmpt  47523  smfliminfmpt  47526  smfsupdmmbllem  47538  finfdm  47540  smfinfdmmbllem  47542  setrec2mpt  50452  aacllem  50578