MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpt2 Structured version   Visualization version   GIF version

Theorem fvmpt2 6083
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
StepHypRef Expression
1 mptrcl.1 . . 3 𝐹 = (𝑥𝐴𝐵)
21fvmpt2i 6082 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6048 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2568 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  cmpt 4541   I cid 4842  cfv 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5653  df-fun 5691  df-fv 5697
This theorem is referenced by:  fvmptss  6084  fvmpt2d  6085  fvmptdf  6087  mpteqb  6090  fvmptt  6091  fvmptf  6092  fnmptfvd  6111  ralrnmpt  6159  fmptco  6186  f1mpt  6295  offval2  6687  ofrfval2  6688  mptelixpg  7706  dom2lem  7756  mapxpen  7886  xpmapenlem  7887  cnfcom3clem  8360  tcvalg  8372  rankf  8415  infxpenc2lem2  8601  dfac8clem  8613  acni2  8627  acnlem  8629  fin23lem32  8924  axcc2lem  9016  axcc3  9018  domtriomlem  9022  ac6num  9059  konigthlem  9144  rpnnen1lem1  11556  rpnnen1lem3  11557  rpnnen1lem5  11559  rpnnen1lem1OLD  11562  rpnnen1lem3OLD  11563  rpnnen1lem5OLD  11565  seqof  12587  seqof2  12588  rlim2  13939  ello1mpt  13964  o1compt  14030  sumrblem  14156  fsumcvg  14157  summolem2a  14160  fsum  14165  fsumcvg2  14172  fsumadd  14184  isummulc2  14202  fsummulc2  14225  fsumrelem  14247  prodrblem  14365  fprodcvg  14366  prodmolem2a  14370  zprod  14373  fprod  14377  fprodmul  14396  fproddiv  14397  iserodd  15260  prmrec  15346  prdsbas3  15846  prdsdsval2  15849  invfuc  16347  yonedalem4c  16630  gsumconst  18062  prdsgsum  18105  gsumdixp  18337  evlslem4  19231  elptr2  21088  ptunimpt  21109  ptcldmpt  21128  ptclsg  21129  txcnp  21134  ptcnplem  21135  cnmpt11  21177  cnmpt1t  21179  cnmptk2  21200  xkocnv  21328  flfcnp2  21522  ustn0  21735  utopsnneiplem  21762  ucnima  21796  iccpnfcnv  22472  ovolctb  22941  ovoliunlem1  22953  ovoliun2  22957  ovolshftlem1  22960  ovolscalem1  22964  voliun  23005  ioombl1lem3  23011  ioombl1lem4  23012  uniioombllem2  23033  mbfeqalem  23091  mbfpos  23100  mbfposr  23101  mbfposb  23102  mbfsup  23113  mbfinf  23114  mbflim  23117  i1fposd  23156  itg1climres  23163  mbfi1fseqlem4  23167  mbfi1fseqlem5  23168  mbfi1fseqlem6  23169  itg2split  23198  itg2mono  23202  itg2cnlem1  23210  isibl2  23215  itgmpt  23231  itgeqa  23262  itggt0  23290  itgcn  23291  limcmpt  23329  dvlipcn  23437  lhop2  23458  dvfsumabs  23466  itgparts  23490  itgsubstlem  23491  itgsubst  23492  elplyd  23647  coeeulem  23669  coeeq2  23687  dvply1  23728  plyremlem  23748  ulmss  23843  ulmdvlem1  23846  mtest  23850  itgulm2  23855  radcnvlem1  23859  pserulm  23868  leibpi  24357  rlimcnp  24380  o1cxp  24389  lgamgulmlem2  24444  lgamgulmlem6  24448  lgamgulm2  24450  sqff1o  24598  lgseisenlem2  24791  dchrvmasumlem1  24874  frgrancvvdeqlem6  26301  ubthlem1  26889  cnlnadjlem5  28103  xppreima2  28619  abfmpunirn  28621  aciunf1lem  28633  fpwrelmap  28685  fimaproj  29025  xrmulc1cn  29101  esumpcvgval  29264  esumsup  29275  voliune  29416  eulerpartgbij  29569  signsplypnf  29799  iscvm  30341  mclsrcl  30558  f1omptsnlem  32191  matunitlindflem2  32451  itg2addnclem  32506  itggt0cn  32527  ftc1anclem5  32534  elrfirn2  36152  eq0rabdioph  36233  monotoddzz  36401  aomclem2  36518  refsumcn  38094  refsum2cnlem1  38101  fvmpt2bd  38228  wessf1ornlem  38250  fompt  38258  projf1o  38265  choicefi  38271  axccdom  38295  fsumsermpt  38532  fmuldfeqlem1  38535  fmuldfeq  38536  climneg  38563  climdivf  38565  mullimc  38569  idlimc  38579  sumnnodd  38583  neglimc  38601  addlimc  38602  0ellimcdiv  38603  cncfmptssg  38642  cncfshift  38646  icccncfext  38660  cncfiooicclem1  38666  fprodsubrecnncnvlem  38681  fprodaddrecnncnvlem  38683  ioodvbdlimc1lem2  38709  ioodvbdlimc1lem2OLD  38711  ioodvbdlimc2lem  38713  ioodvbdlimc2lemOLD  38714  dvnmptdivc  38718  dvnmul  38723  dvnprodlem2  38727  itgsin0pilem1  38731  ibliccsinexp  38732  itgsinexplem1  38735  itgsinexp  38736  ditgeqiooicc  38742  itgsubsticclem  38757  itgioocnicc  38759  stoweidlem2  38785  stoweidlem11  38794  stoweidlem12  38795  stoweidlem16  38799  stoweidlem17  38800  stoweidlem18  38801  stoweidlem19  38802  stoweidlem20  38803  stoweidlem21  38804  stoweidlem22  38805  stoweidlem23  38806  stoweidlem27  38810  stoweidlem31  38814  stoweidlem34  38817  stoweidlem36  38819  stoweidlem40  38823  stoweidlem41  38824  stoweidlem42  38825  stoweidlem48  38831  stoweidlem55  38838  stoweidlem59  38842  stoweidlem62  38845  stirlinglem3  38859  stirlinglem8  38864  stirlinglem14  38870  stirlinglem15  38871  stirlingr  38873  dirkeritg  38885  dirkercncflem2  38887  fourierdlem14  38904  fourierdlem31  38921  fourierdlem31OLD  38922  fourierdlem41  38932  fourierdlem48  38939  fourierdlem49  38940  fourierdlem50  38941  fourierdlem51  38942  fourierdlem56  38947  fourierdlem60  38951  fourierdlem61  38952  fourierdlem66  38957  fourierdlem70  38961  fourierdlem71  38962  fourierdlem73  38964  fourierdlem74  38965  fourierdlem75  38966  fourierdlem76  38967  fourierdlem77  38968  fourierdlem78  38969  fourierdlem81  38972  fourierdlem83  38974  fourierdlem84  38975  fourierdlem85  38976  fourierdlem87  38978  fourierdlem88  38979  fourierdlem89  38980  fourierdlem91  38982  fourierdlem92  38983  fourierdlem93  38984  fourierdlem95  38986  fourierdlem97  38988  fourierdlem101  38992  fourierdlem103  38994  fourierdlem104  38995  fourierdlem111  39002  fourierdlem112  39003  sqwvfoura  39013  sqwvfourb  39014  fouriersw  39016  elaa2lem  39018  elaa2lemOLD  39019  etransclem4  39024  etransclem13  39033  etransclem35  39055  etransclem46  39066  etransclem48OLD  39068  etransclem48  39069  sge0revalmpt  39165  sge0fsummpt  39177  sge0iunmptlemfi  39200  sge0iunmptlemre  39202  sge0ltfirpmpt2  39213  sge0fsummptf  39223  nnfoctbdjlem  39242  iundjiun  39247  meaiunlelem  39255  meaiuninclem  39267  omeiunlempt  39304  carageniuncllem2  39306  caratheodorylem2  39311  0ome  39313  isomenndlem  39314  hoicvr  39332  hoicvrrex  39340  ovn0lem  39349  ovnsubaddlem1  39354  hoidmvlelem2  39380  hoidmvlelem3  39381  ovnhoilem2  39386  hoicoto2  39389  hoi2toco  39391  ovnlecvr2  39394  ovncvr2  39395  ovnsubadd2lem  39429  ovolval5lem2  39437  ovnovollem1  39440  ovnovollem2  39441  vonioolem1  39465  smfaddlem1  39543  smflimlem2  39552  frgrncvvdeqlem6  41566  aacllem  42409
  Copyright terms: Public domain W3C validator