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

Theorem fvmpt2 6024
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 6023 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 5989 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2559 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378   = wceq 1468  wcel 1937  cmpt 4493   I cid 4790  cfv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-mpt 4495  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5597  df-fun 5635  df-fv 5641
This theorem is referenced by:  fvmptss  6025  fvmpt2d  6026  fvmptdf  6028  mpteqb  6031  fvmptt  6032  fvmptf  6033  fnmptfvd  6052  ralrnmpt  6098  fmptco  6124  f1mpt  6233  offval2  6624  ofrfval2  6625  mptelixpg  7642  dom2lem  7692  mapxpen  7822  xpmapenlem  7823  cnfcom3clem  8295  tcvalg  8307  rankf  8350  infxpenc2lem2  8536  dfac8clem  8548  acni2  8562  acnlem  8564  fin23lem32  8859  axcc2lem  8951  axcc3  8953  domtriomlem  8957  ac6num  8994  konigthlem  9078  rpnnen1lem1  11381  rpnnen1lem3  11383  rpnnen1lem5  11385  seqof  12384  seqof2  12385  rlim2  13720  ello1mpt  13745  o1compt  13811  sumrblem  13937  fsumcvg  13938  summolem2a  13941  fsum  13946  fsumcvg2  13953  fsumadd  13965  isummulc2  13983  fsummulc2  14005  fsumrelem  14027  prodrblem  14143  fprodcvg  14144  prodmolem2a  14148  zprod  14151  fprod  14155  fprodmul  14174  fproddiv  14175  iserodd  14947  prmrec  15028  prdsbas3  15544  prdsdsval2  15547  invfuc  16045  yonedalem4c  16328  gsumconst  17728  prdsgsum  17771  gsumdixp  17997  evlslem4  18890  elptr2  20746  ptunimpt  20767  ptcldmpt  20786  ptclsg  20787  txcnp  20792  ptcnplem  20793  cnmpt11  20835  cnmpt1t  20837  cnmptk2  20858  xkocnv  20986  flfcnp2  21180  ustn0  21393  utopsnneiplem  21420  ucnima  21454  iccpnfcnv  22130  ovolctb  22602  ovoliunlem1  22614  ovoliun2  22618  ovolshftlem1  22621  ovolscalem1  22625  voliun  22667  ioombl1lem3  22673  ioombl1lem4  22674  uniioombllem2  22700  uniioombllem2OLD  22701  mbfeqalem  22759  mbfpos  22768  mbfposr  22769  mbfposb  22770  mbfsup  22781  mbfinf  22782  mbfinfOLD  22783  mbflim  22787  i1fposd  22826  itg1climres  22833  mbfi1fseqlem4  22837  mbfi1fseqlem5  22838  mbfi1fseqlem6  22839  itg2split  22868  itg2mono  22872  itg2cnlem1  22880  isibl2  22885  itgmpt  22901  itgeqa  22932  itggt0  22960  itgcn  22961  limcmpt  22999  dvlipcn  23107  lhop2  23128  dvfsumabs  23136  itgparts  23160  itgsubstlem  23161  itgsubst  23162  elplyd  23317  coeeulem  23339  coeeq2  23357  dvply1  23398  plyremlem  23418  ulmss  23513  ulmdvlem1  23516  mtest  23520  itgulm2  23525  radcnvlem1  23529  pserulm  23538  leibpi  24029  rlimcnp  24052  o1cxp  24061  lgamgulmlem2  24116  lgamgulmlem6  24120  lgamgulm2  24122  sqff1o  24270  lgseisenlem2  24439  dchrvmasumlem1  24494  frgrancvvdeqlem6  25923  ubthlem1  26675  cnlnadjlem5  27887  xppreima2  28407  abfmpunirn  28409  aciunf1lem  28421  fpwrelmap  28474  fimaproj  28815  xrmulc1cn  28891  esumpcvgval  29054  esumsup  29065  voliune  29206  eulerpartgbij  29359  signsplypnf  29592  iscvm  30134  mclsrcl  30351  f1omptsnlem  31959  matunitlindflem2  32175  itg2addnclem  32231  itggt0cn  32252  ftc1anclem5  32259  elrfirn2  35778  eq0rabdioph  35859  monotoddzz  36031  aomclem2  36153  refsumcn  37699  refsum2cnlem1  37706  fvmpt2bd  37797  wessf1ornlem  37819  fompt  37827  projf1o  37834  choicefi  37840  fsumsermpt  38059  fmuldfeqlem1  38062  fmuldfeq  38063  climneg  38093  climdivf  38096  mullimc  38100  idlimc  38110  sumnnodd  38114  neglimc  38132  addlimc  38133  0ellimcdiv  38134  cncfmptssg  38156  cncfshift  38160  icccncfext  38174  cncfiooicclem1  38180  fprodsubrecnncnvlem  38195  fprodaddrecnncnvlem  38197  ioodvbdlimc1lem2  38223  ioodvbdlimc1lem2OLD  38225  ioodvbdlimc2lem  38227  ioodvbdlimc2lemOLD  38228  dvnmptdivc  38232  dvnmul  38237  dvnprodlem2  38241  itgsin0pilem1  38245  ibliccsinexp  38246  itgsinexplem1  38249  itgsinexp  38250  ditgeqiooicc  38256  itgsubsticclem  38271  itgioocnicc  38273  stoweidlem2  38298  stoweidlem11  38307  stoweidlem12  38308  stoweidlem16  38312  stoweidlem17  38313  stoweidlem18  38314  stoweidlem19  38315  stoweidlem20  38316  stoweidlem21  38317  stoweidlem22  38318  stoweidlem23  38319  stoweidlem27  38323  stoweidlem31  38328  stoweidlem34  38331  stoweidlem36  38333  stoweidlem40  38337  stoweidlem41  38338  stoweidlem42  38339  stoweidlem48  38345  stoweidlem55  38352  stoweidlem59  38356  stoweidlem62  38359  stoweidlem62OLD  38360  stirlinglem3  38374  stirlinglem8  38379  stirlinglem14  38385  stirlinglem15  38386  stirlingr  38388  dirkeritg  38400  dirkercncflem2  38402  fourierdlem14  38419  fourierdlem31  38436  fourierdlem31OLD  38437  fourierdlem41  38447  fourierdlem48  38454  fourierdlem49  38455  fourierdlem50  38456  fourierdlem51  38457  fourierdlem56  38462  fourierdlem60  38466  fourierdlem61  38467  fourierdlem66  38472  fourierdlem70  38476  fourierdlem71  38477  fourierdlem73  38479  fourierdlem74  38480  fourierdlem75  38481  fourierdlem76  38482  fourierdlem77  38483  fourierdlem78  38484  fourierdlem81  38487  fourierdlem83  38489  fourierdlem84  38490  fourierdlem85  38491  fourierdlem87  38493  fourierdlem88  38494  fourierdlem89  38495  fourierdlem91  38497  fourierdlem92  38498  fourierdlem93  38499  fourierdlem95  38501  fourierdlem97  38503  fourierdlem101  38507  fourierdlem103  38509  fourierdlem104  38510  fourierdlem111  38517  fourierdlem112  38518  sqwvfoura  38528  sqwvfourb  38529  fouriersw  38531  elaa2lem  38533  elaa2lemOLD  38534  etransclem4  38539  etransclem13  38548  etransclem35  38570  etransclem46  38581  etransclem48OLD  38583  etransclem48  38584  sge0revalmpt  38666  sge0fsummpt  38678  sge0iunmptlemfi  38701  sge0iunmptlemre  38703  sge0ltfirpmpt2  38714  sge0fsummptf  38724  nnfoctbdjlem  38743  iundjiun  38748  meaiunlelem  38756  meaiuninclem  38768  omeiunlempt  38805  carageniuncllem2  38807  caratheodorylem2  38812  0ome  38814  isomenndlem  38815  hoicvr  38833  hoicvrrex  38841  ovn0lem  38850  ovnsubaddlem1  38855  hoidmvlelem2  38881  hoidmvlelem3  38882  ovnhoilem2  38887  hoicoto2  38890  hoi2toco  38892  ovnlecvr2  38895  ovncvr2  38896  ovnsubadd2lem  38930  ovolval5lem2  38938  ovnovollem1  38941  ovnovollem2  38942  vonioolem1  38966  frgrncvvdeqlem6  40874  aacllem  41727
  Copyright terms: Public domain W3C validator