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

Theorem fvmpt2 6200
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 6199 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6165 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2664 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  cmpt 4643   I cid 4948  cfv 5804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812
This theorem is referenced by:  fvmptss  6201  fvmpt2d  6202  fvmptdf  6204  mpteqb  6207  fvmptt  6208  fvmptf  6209  fnmptfvd  6228  ralrnmpt  6276  fmptco  6303  f1mpt  6419  offval2  6812  ofrfval2  6813  mptelixpg  7831  dom2lem  7881  mapxpen  8011  xpmapenlem  8012  cnfcom3clem  8485  tcvalg  8497  rankf  8540  infxpenc2lem2  8726  dfac8clem  8738  acni2  8752  acnlem  8754  fin23lem32  9049  axcc2lem  9141  axcc3  9143  domtriomlem  9147  ac6num  9184  konigthlem  9269  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  seqof  12720  seqof2  12721  rlim2  14075  ello1mpt  14100  o1compt  14166  sumrblem  14289  fsumcvg  14290  summolem2a  14293  fsum  14298  fsumcvg2  14305  fsumadd  14317  isummulc2  14335  fsummulc2  14358  fsumrelem  14380  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  fprod  14510  fprodmul  14529  fproddiv  14530  iserodd  15378  prmrec  15464  prdsbas3  15964  prdsdsval2  15967  invfuc  16457  yonedalem4c  16740  gsumconst  18157  prdsgsum  18200  gsumdixp  18432  evlslem4  19329  elptr2  21187  ptunimpt  21208  ptcldmpt  21227  ptclsg  21228  txcnp  21233  ptcnplem  21234  cnmpt11  21276  cnmpt1t  21278  cnmptk2  21299  xkocnv  21427  flfcnp2  21621  ustn0  21834  utopsnneiplem  21861  ucnima  21895  iccpnfcnv  22551  ovolctb  23065  ovoliunlem1  23077  ovoliun2  23081  ovolshftlem1  23084  ovolscalem1  23088  voliun  23129  ioombl1lem3  23135  ioombl1lem4  23136  uniioombllem2  23157  mbfeqalem  23215  mbfpos  23224  mbfposr  23225  mbfposb  23226  mbfsup  23237  mbfinf  23238  mbflim  23241  i1fposd  23280  itg1climres  23287  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2split  23322  itg2mono  23326  itg2cnlem1  23334  isibl2  23339  itgmpt  23355  itgeqa  23386  itggt0  23414  itgcn  23415  limcmpt  23453  dvlipcn  23561  lhop2  23582  dvfsumabs  23590  itgparts  23614  itgsubstlem  23615  itgsubst  23616  elplyd  23762  coeeulem  23784  coeeq2  23802  dvply1  23843  plyremlem  23863  ulmss  23955  ulmdvlem1  23958  mtest  23962  itgulm2  23967  radcnvlem1  23971  pserulm  23980  leibpi  24469  rlimcnp  24492  o1cxp  24501  lgamgulmlem2  24556  lgamgulmlem6  24560  lgamgulm2  24562  sqff1o  24708  lgseisenlem2  24901  dchrvmasumlem1  24984  frgrancvvdeqlem6  26562  ubthlem1  27110  cnlnadjlem5  28314  xppreima2  28830  abfmpunirn  28832  aciunf1lem  28844  fpwrelmap  28896  fimaproj  29228  xrmulc1cn  29304  esumpcvgval  29467  esumsup  29478  voliune  29619  eulerpartgbij  29761  signsplypnf  29953  iscvm  30495  mclsrcl  30712  f1omptsnlem  32359  matunitlindflem2  32576  itg2addnclem  32631  itggt0cn  32652  ftc1anclem5  32659  elrfirn2  36277  eq0rabdioph  36358  monotoddzz  36526  aomclem2  36643  refsumcn  38212  refsum2cnlem1  38219  fvmpt2bd  38345  wessf1ornlem  38366  fompt  38374  projf1o  38381  choicefi  38387  axccdom  38411  fsumsermpt  38646  fmuldfeqlem1  38649  fmuldfeq  38650  climneg  38677  climdivf  38679  mullimc  38683  idlimc  38693  sumnnodd  38697  neglimc  38714  addlimc  38715  0ellimcdiv  38716  cncfmptssg  38755  cncfshift  38759  icccncfext  38773  cncfiooicclem1  38779  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmptdivc  38828  dvnmul  38833  dvnprodlem2  38837  itgsin0pilem1  38841  ibliccsinexp  38842  itgsinexplem1  38845  itgsinexp  38846  ditgeqiooicc  38852  itgsubsticclem  38867  itgioocnicc  38869  stoweidlem2  38895  stoweidlem11  38904  stoweidlem12  38905  stoweidlem16  38909  stoweidlem17  38910  stoweidlem18  38911  stoweidlem19  38912  stoweidlem20  38913  stoweidlem21  38914  stoweidlem22  38915  stoweidlem23  38916  stoweidlem27  38920  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem40  38933  stoweidlem41  38934  stoweidlem42  38935  stoweidlem48  38941  stoweidlem55  38948  stoweidlem59  38952  stoweidlem62  38955  stirlinglem3  38969  stirlinglem8  38974  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  dirkeritg  38995  dirkercncflem2  38997  fourierdlem14  39014  fourierdlem31  39031  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem56  39055  fourierdlem60  39059  fourierdlem61  39060  fourierdlem66  39065  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem77  39076  fourierdlem78  39077  fourierdlem81  39080  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem87  39086  fourierdlem88  39087  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  elaa2lem  39126  etransclem4  39131  etransclem13  39140  etransclem35  39162  etransclem46  39173  etransclem48  39175  sge0revalmpt  39271  sge0fsummpt  39283  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0ltfirpmpt2  39319  sge0fsummptf  39329  nnfoctbdjlem  39348  iundjiun  39353  meaiunlelem  39361  meaiuninclem  39373  omeiunlempt  39410  carageniuncllem2  39412  caratheodorylem2  39417  0ome  39419  isomenndlem  39420  hoicvr  39438  hoicvrrex  39446  ovn0lem  39455  ovnsubaddlem1  39460  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem2  39492  hoicoto2  39495  hoi2toco  39497  ovnlecvr2  39500  ovncvr2  39501  ovnsubadd2lem  39535  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  vonioolem1  39571  smfaddlem1  39649  smflimlem2  39658  frgrncvvdeqlem6  41474  aacllem  42356
  Copyright terms: Public domain W3C validator