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

Theorem fvmpt2 6848
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 6847 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6806 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2799 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2111  cmpt 5150   I cid 5469  cfv 6398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pr 5337
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-br 5069  df-opab 5131  df-mpt 5151  df-id 5470  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-iota 6356  df-fun 6400  df-fv 6406
This theorem is referenced by:  fvmptss  6849  fvmpt2d  6850  fvmptd3f  6852  mpteqb  6856  fvmptt  6857  fvmptf  6858  fnmptfvd  6880  ralrnmptw  6932  ralrnmpt  6934  fmptco  6963  f1mpt  7092  offval2  7507  ofrfval2  7508  fimaproj  7923  mptelixpg  8637  dom2lem  8691  mapxpen  8835  xpmapenlem  8836  cnfcom3clem  9345  tcvalg  9379  rankf  9435  infxpenc2lem2  9659  dfac8clem  9671  acni2  9685  acnlem  9687  fin23lem32  9983  axcc2lem  10075  axcc3  10077  domtriomlem  10081  ac6num  10118  konigthlem  10207  rpnnen1lem1  12599  rpnnen1lem3  12600  rpnnen1lem5  12602  seqof  13658  seqof2  13659  rlim2  15082  ello1mpt  15107  o1compt  15173  sumrblem  15300  fsumcvg  15301  summolem2a  15304  fsum  15309  fsumcvg2  15316  fsumadd  15329  isummulc2  15351  fsummulc2  15373  fsumrelem  15396  prodrblem  15516  fprodcvg  15517  prodmolem2a  15521  zprod  15524  fprod  15528  fprodmul  15547  fproddiv  15548  iserodd  16413  prmrec  16500  prdsbas3  17011  prdsdsval2  17014  invfuc  17508  yonedalem4c  17810  smndex1n0mnd  18364  gsumconst  19344  prdsgsum  19391  gsumdixp  19652  evlslem4  21058  elptr2  22495  ptunimpt  22516  ptcldmpt  22535  ptclsg  22536  txcnp  22541  ptcnplem  22542  cnmpt11  22584  cnmpt1t  22586  cnmptk2  22607  xkocnv  22735  flfcnp2  22928  ustn0  23142  utopsnneiplem  23169  ucnima  23202  iccpnfcnv  23865  ovolctb  24411  ovoliunlem1  24423  ovoliun2  24427  ovolshftlem1  24430  ovolscalem1  24434  voliun  24475  ioombl1lem3  24481  ioombl1lem4  24482  uniioombllem2  24504  mbfeqalem1  24562  mbfpos  24572  mbfposr  24573  mbfposb  24574  mbfsup  24585  mbfinf  24586  mbflim  24589  i1fposd  24629  itg1climres  24636  mbfi1fseqlem4  24640  mbfi1fseqlem5  24641  mbfi1fseqlem6  24642  itg2split  24671  itg2mono  24675  itg2cnlem1  24683  isibl2  24688  itgmpt  24704  itgeqa  24735  itggt0  24765  itgcn  24766  limcmpt  24804  dvlipcn  24915  lhop2  24936  dvfsumabs  24944  itgparts  24968  itgsubstlem  24969  itgsubst  24970  elplyd  25120  coeeulem  25142  coeeq2  25160  dvply1  25201  plyremlem  25221  ulmss  25313  ulmdvlem1  25316  mtest  25320  itgulm2  25325  radcnvlem1  25329  pserulm  25338  leibpi  25849  rlimcnp  25872  o1cxp  25881  lgamgulmlem2  25936  lgamgulmlem6  25940  lgamgulm2  25942  sqff1o  26088  lgseisenlem2  26281  dchrvmasumlem1  26400  frgrncvvdeqlem5  28410  ubthlem1  28975  cnlnadjlem5  30176  xppreima2  30731  abfmpunirn  30733  aciunf1lem  30743  suppovss  30761  fpwrelmap  30812  nsgmgc  31335  xrmulc1cn  31618  esumpcvgval  31782  esumsup  31793  voliune  31933  eulerpartgbij  32075  signsplypnf  32265  iscvm  32957  mclsrcl  33259  f1omptsnlem  35271  matunitlindflem2  35538  itg2addnclem  35592  itggt0cn  35611  ftc1anclem5  35618  pwsgprod  40010  elrfirn2  40250  eq0rabdioph  40330  monotoddzz  40497  aomclem2  40612  refsumcn  42275  refsum2cnlem1  42282  fvmpt2bd  42408  fompt  42432  choicefi  42442  axccdom  42464  fvmpt4  42483  fsumsermpt  42824  fmuldfeqlem1  42827  fmuldfeq  42828  climneg  42855  climdivf  42857  mullimc  42861  idlimc  42871  sumnnodd  42875  neglimc  42892  addlimc  42893  0ellimcdiv  42894  climfveqmpt2  42938  climeqmpt  42942  limsupequzmptlem  42973  liminfvalxr  43028  xlimmnfmpt  43088  xlimpnfmpt  43089  cncfmptssg  43116  cncfshift  43119  icccncfext  43132  cncfiooicclem1  43138  fprodsubrecnncnvlem  43152  fprodaddrecnncnvlem  43154  ioodvbdlimc1lem2  43177  ioodvbdlimc2lem  43179  dvnmptdivc  43183  dvnmul  43188  dvnprodlem2  43192  itgsin0pilem1  43195  ibliccsinexp  43196  itgsinexplem1  43199  itgsinexp  43200  ditgeqiooicc  43205  itgsubsticclem  43220  itgioocnicc  43222  stoweidlem2  43247  stoweidlem11  43256  stoweidlem12  43257  stoweidlem16  43261  stoweidlem17  43262  stoweidlem18  43263  stoweidlem19  43264  stoweidlem20  43265  stoweidlem21  43266  stoweidlem22  43267  stoweidlem23  43268  stoweidlem27  43272  stoweidlem31  43276  stoweidlem34  43279  stoweidlem36  43281  stoweidlem40  43285  stoweidlem41  43286  stoweidlem42  43287  stoweidlem48  43293  stoweidlem55  43300  stoweidlem59  43304  stoweidlem62  43307  stirlinglem3  43321  stirlinglem8  43326  stirlinglem14  43332  stirlinglem15  43333  stirlingr  43335  dirkeritg  43347  dirkercncflem2  43349  fourierdlem14  43366  fourierdlem31  43383  fourierdlem41  43393  fourierdlem48  43399  fourierdlem49  43400  fourierdlem50  43401  fourierdlem51  43402  fourierdlem56  43407  fourierdlem60  43411  fourierdlem61  43412  fourierdlem66  43417  fourierdlem70  43421  fourierdlem71  43422  fourierdlem73  43424  fourierdlem74  43425  fourierdlem75  43426  fourierdlem76  43427  fourierdlem77  43428  fourierdlem78  43429  fourierdlem81  43432  fourierdlem83  43434  fourierdlem84  43435  fourierdlem85  43436  fourierdlem87  43438  fourierdlem88  43439  fourierdlem89  43440  fourierdlem91  43442  fourierdlem92  43443  fourierdlem93  43444  fourierdlem95  43446  fourierdlem97  43448  fourierdlem101  43452  fourierdlem103  43454  fourierdlem104  43455  fourierdlem111  43462  fourierdlem112  43463  sqwvfoura  43473  sqwvfourb  43474  fouriersw  43476  elaa2lem  43478  etransclem4  43483  etransclem13  43492  etransclem35  43514  etransclem46  43525  etransclem48  43527  sge0revalmpt  43620  sge0fsummpt  43632  sge0iunmptlemfi  43655  sge0iunmptlemre  43657  sge0ltfirpmpt2  43668  sge0fsummptf  43678  nnfoctbdjlem  43697  iundjiun  43702  meaiunlelem  43710  meaiuninclem  43722  meaiuninc3v  43726  omeiunlempt  43762  carageniuncllem2  43764  caratheodorylem2  43769  0ome  43771  isomenndlem  43772  hoicvr  43790  hoicvrrex  43798  ovn0lem  43807  ovnsubaddlem1  43812  hoidmvlelem2  43838  hoidmvlelem3  43839  ovnhoilem2  43844  hoicoto2  43847  hoi2toco  43849  ovnlecvr2  43852  ovncvr2  43853  ovnsubadd2lem  43887  ovolval5lem2  43895  ovnovollem1  43898  ovnovollem2  43899  vonioolem1  43922  smfaddlem1  43999  smflimlem2  44008  smflimmpt  44044  smfsupmpt  44049  smfinfmpt  44053  smflimsuplem2  44055  smflimsuplem4  44057  smflimsuplem5  44058  smflimsupmpt  44063  smfliminfmpt  44066  aacllem  46205
  Copyright terms: Public domain W3C validator