Theorem fvmpt2 6434

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145   ↦ cmpt 4864   I cid 5157  ‘cfv 6032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5995  df-fun 6034  df-fv 6040

This theorem is referenced by:  fvmptss  6435  fvmpt2d  6436  fvmptd3f  6438  mpteqb  6442  fvmptt  6443  fvmptf  6444  fnmptfvd  6464  ralrnmpt  6512  fmptco  6540  f1mpt  6662  offval2  7062  ofrfval2  7063  mptelixpg  8100  dom2lem  8150  mapxpen  8283  xpmapenlem  8284  cnfcom3clem  8767  tcvalg  8779  rankf  8822  infxpenc2lem2  9044  dfac8clem  9056  acni2  9070  acnlem  9072  fin23lem32  9369  axcc2lem  9461  axcc3  9463  domtriomlem  9467  ac6num  9504  konigthlem  9593  rpnnen1lem1  12019  rpnnen1lem3  12020  rpnnen1lem5  12022  rpnnen1lem1OLD  12025  rpnnen1lem3OLD  12026  rpnnen1lem5OLD  12028  seqof  13066  seqof2  13067  rlim2  14436  ello1mpt  14461  o1compt  14527  sumrblem  14651  fsumcvg  14652  summolem2a  14655  fsum  14660  fsumcvg2  14667  fsumadd  14679  isummulc2  14702  fsummulc2  14724  fsumrelem  14747  prodrblem  14867  fprodcvg  14868  prodmolem2a  14872  zprod  14875  fprod  14879  fprodmul  14898  fproddiv  14899  iserodd  15748  prmrec  15834  prdsbas3  16350  prdsdsval2  16353  invfuc  16842  yonedalem4c  17126  gsumconst  18542  prdsgsum  18585  gsumdixp  18818  evlslem4  19724  elptr2  21599  ptunimpt  21620  ptcldmpt  21639  ptclsg  21640  txcnp  21645  ptcnplem  21646  cnmpt11  21688  cnmpt1t  21690  cnmptk2  21711  xkocnv  21839  flfcnp2  22032  ustn0  22245  utopsnneiplem  22272  ucnima  22306  iccpnfcnv  22964  ovolctb  23479  ovoliunlem1  23491  ovoliun2  23495  ovolshftlem1  23498  ovolscalem1  23502  voliun  23543  ioombl1lem3  23549  ioombl1lem4  23550  uniioombllem2  23572  mbfeqalem  23630  mbfpos  23639  mbfposr  23640  mbfposb  23641  mbfsup  23652  mbfinf  23653  mbflim  23656  i1fposd  23695  itg1climres  23702  mbfi1fseqlem4  23706  mbfi1fseqlem5  23707  mbfi1fseqlem6  23708  itg2split  23737  itg2mono  23741  itg2cnlem1  23749  isibl2  23754  itgmpt  23770  itgeqa  23801  itggt0  23829  itgcn  23830  limcmpt  23868  dvlipcn  23978  lhop2  23999  dvfsumabs  24007  itgparts  24031  itgsubstlem  24032  itgsubst  24033  elplyd  24179  coeeulem  24201  coeeq2  24219  dvply1  24260  plyremlem  24280  ulmss  24372  ulmdvlem1  24375  mtest  24379  itgulm2  24384  radcnvlem1  24388  pserulm  24397  leibpi  24891  rlimcnp  24914  o1cxp  24923  lgamgulmlem2  24978  lgamgulmlem6  24982  lgamgulm2  24984  sqff1o  25130  lgseisenlem2  25323  dchrvmasumlem1  25406  frgrncvvdeqlem5  27486  ubthlem1  28067  cnlnadjlem5  29271  xppreima2  29791  abfmpunirn  29793  aciunf1lem  29803  fpwrelmap  29849  fimaproj  30241  xrmulc1cn  30317  esumpcvgval  30481  esumsup  30492  voliune  30633  eulerpartgbij  30775  signsplypnf  30968  iscvm  31580  mclsrcl  31797  f1omptsnlem  33521  matunitlindflem2  33740  itg2addnclem  33794  itggt0cn  33815  ftc1anclem5  33822  elrfirn2  37786  eq0rabdioph  37867  monotoddzz  38035  aomclem2  38152  refsumcn  39712  refsum2cnlem1  39719  fvmpt2bd  39871  wessf1ornlem  39892  fompt  39900  projf1o  39907  choicefi  39911  axccdom  39935  fvmpt4  39965  fsumsermpt  40330  fmuldfeqlem1  40333  fmuldfeq  40334  climneg  40361  climdivf  40363  mullimc  40367  idlimc  40377  sumnnodd  40381  neglimc  40398  addlimc  40399  0ellimcdiv  40400  climfveqmpt2  40444  climeqmpt  40448  limsupequzmptlem  40479  liminfvalxr  40534  xlimmnfmpt  40588  xlimpnfmpt  40589  cncfmptssg  40602  cncfshift  40606  icccncfext  40619  cncfiooicclem1  40625  fprodsubrecnncnvlem  40640  fprodaddrecnncnvlem  40642  ioodvbdlimc1lem2  40666  ioodvbdlimc2lem  40668  dvnmptdivc  40672  dvnmul  40677  dvnprodlem2  40681  itgsin0pilem1  40684  ibliccsinexp  40685  itgsinexplem1  40688  itgsinexp  40689  ditgeqiooicc  40694  itgsubsticclem  40709  itgioocnicc  40711  stoweidlem2  40737  stoweidlem11  40746  stoweidlem12  40747  stoweidlem16  40751  stoweidlem17  40752  stoweidlem18  40753  stoweidlem19  40754  stoweidlem20  40755  stoweidlem21  40756  stoweidlem22  40757  stoweidlem23  40758  stoweidlem27  40762  stoweidlem31  40766  stoweidlem34  40769  stoweidlem36  40771  stoweidlem40  40775  stoweidlem41  40776  stoweidlem42  40777  stoweidlem48  40783  stoweidlem55  40790  stoweidlem59  40794  stoweidlem62  40797  stirlinglem3  40811  stirlinglem8  40816  stirlinglem14  40822  stirlinglem15  40823  stirlingr  40825  dirkeritg  40837  dirkercncflem2  40839  fourierdlem14  40856  fourierdlem31  40873  fourierdlem41  40883  fourierdlem48  40889  fourierdlem49  40890  fourierdlem50  40891  fourierdlem51  40892  fourierdlem56  40897  fourierdlem60  40901  fourierdlem61  40902  fourierdlem66  40907  fourierdlem70  40911  fourierdlem71  40912  fourierdlem73  40914  fourierdlem74  40915  fourierdlem75  40916  fourierdlem76  40917  fourierdlem77  40918  fourierdlem78  40919  fourierdlem81  40922  fourierdlem83  40924  fourierdlem84  40925  fourierdlem85  40926  fourierdlem87  40928  fourierdlem88  40929  fourierdlem89  40930  fourierdlem91  40932  fourierdlem92  40933  fourierdlem93  40934  fourierdlem95  40936  fourierdlem97  40938  fourierdlem101  40942  fourierdlem103  40944  fourierdlem104  40945  fourierdlem111  40952  fourierdlem112  40953  sqwvfoura  40963  sqwvfourb  40964  fouriersw  40966  elaa2lem  40968  etransclem4  40973  etransclem13  40982  etransclem35  41004  etransclem46  41015  etransclem48  41017  sge0revalmpt  41113  sge0fsummpt  41125  sge0iunmptlemfi  41148  sge0iunmptlemre  41150  sge0ltfirpmpt2  41161  sge0fsummptf  41171  nnfoctbdjlem  41190  iundjiun  41195  meaiunlelem  41203  meaiuninclem  41215  meaiuninc3v  41219  omeiunlempt  41255  carageniuncllem2  41257  caratheodorylem2  41262  0ome  41264  isomenndlem  41265  hoicvr  41283  hoicvrrex  41291  ovn0lem  41300  ovnsubaddlem1  41305  hoidmvlelem2  41331  hoidmvlelem3  41332  ovnhoilem2  41337  hoicoto2  41340  hoi2toco  41342  ovnlecvr2  41345  ovncvr2  41346  ovnsubadd2lem  41380  ovolval5lem2  41388  ovnovollem1  41391  ovnovollem2  41392  vonioolem1  41415  smfaddlem1  41492  smflimlem2  41501  smflimmpt  41537  smfsupmpt  41542  smfinfmpt  41546  smflimsuplem2  41548  smflimsuplem4  41550  smflimsuplem5  41551  smflimsupmpt  41556  smfliminfmpt  41559  aacllem  43079