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

Theorem fvmpt2 6258
 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 6257 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6222 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2675 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ↦ cmpt 4683   I cid 4994  ‘cfv 5857 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fv 5865 This theorem is referenced by:  fvmptss  6259  fvmpt2d  6260  fvmptdf  6262  mpteqb  6265  fvmptt  6266  fvmptf  6267  fnmptfvd  6286  ralrnmpt  6334  fmptco  6362  f1mpt  6483  offval2  6879  ofrfval2  6880  mptelixpg  7905  dom2lem  7955  mapxpen  8086  xpmapenlem  8087  cnfcom3clem  8562  tcvalg  8574  rankf  8617  infxpenc2lem2  8803  dfac8clem  8815  acni2  8829  acnlem  8831  fin23lem32  9126  axcc2lem  9218  axcc3  9220  domtriomlem  9224  ac6num  9261  konigthlem  9350  rpnnen1lem1  11775  rpnnen1lem3  11776  rpnnen1lem5  11778  rpnnen1lem1OLD  11781  rpnnen1lem3OLD  11782  rpnnen1lem5OLD  11784  seqof  12814  seqof2  12815  rlim2  14177  ello1mpt  14202  o1compt  14268  sumrblem  14391  fsumcvg  14392  summolem2a  14395  fsum  14400  fsumcvg2  14407  fsumadd  14419  isummulc2  14440  fsummulc2  14463  fsumrelem  14485  prodrblem  14603  fprodcvg  14604  prodmolem2a  14608  zprod  14611  fprod  14615  fprodmul  14634  fproddiv  14635  iserodd  15483  prmrec  15569  prdsbas3  16081  prdsdsval2  16084  invfuc  16574  yonedalem4c  16857  gsumconst  18274  prdsgsum  18317  gsumdixp  18549  evlslem4  19448  elptr2  21317  ptunimpt  21338  ptcldmpt  21357  ptclsg  21358  txcnp  21363  ptcnplem  21364  cnmpt11  21406  cnmpt1t  21408  cnmptk2  21429  xkocnv  21557  flfcnp2  21751  ustn0  21964  utopsnneiplem  21991  ucnima  22025  iccpnfcnv  22683  ovolctb  23198  ovoliunlem1  23210  ovoliun2  23214  ovolshftlem1  23217  ovolscalem1  23221  voliun  23262  ioombl1lem3  23268  ioombl1lem4  23269  uniioombllem2  23291  mbfeqalem  23349  mbfpos  23358  mbfposr  23359  mbfposb  23360  mbfsup  23371  mbfinf  23372  mbflim  23375  i1fposd  23414  itg1climres  23421  mbfi1fseqlem4  23425  mbfi1fseqlem5  23426  mbfi1fseqlem6  23427  itg2split  23456  itg2mono  23460  itg2cnlem1  23468  isibl2  23473  itgmpt  23489  itgeqa  23520  itggt0  23548  itgcn  23549  limcmpt  23587  dvlipcn  23695  lhop2  23716  dvfsumabs  23724  itgparts  23748  itgsubstlem  23749  itgsubst  23750  elplyd  23896  coeeulem  23918  coeeq2  23936  dvply1  23977  plyremlem  23997  ulmss  24089  ulmdvlem1  24092  mtest  24096  itgulm2  24101  radcnvlem1  24105  pserulm  24114  leibpi  24603  rlimcnp  24626  o1cxp  24635  lgamgulmlem2  24690  lgamgulmlem6  24694  lgamgulm2  24696  sqff1o  24842  lgseisenlem2  25035  dchrvmasumlem1  25118  frgrncvvdeqlem6  27066  ubthlem1  27614  cnlnadjlem5  28818  xppreima2  29333  abfmpunirn  29335  aciunf1lem  29345  fpwrelmap  29392  fimaproj  29724  xrmulc1cn  29800  esumpcvgval  29963  esumsup  29974  voliune  30115  eulerpartgbij  30257  signsplypnf  30449  iscvm  31002  mclsrcl  31219  f1omptsnlem  32854  matunitlindflem2  33077  itg2addnclem  33132  itggt0cn  33153  ftc1anclem5  33160  elrfirn2  36778  eq0rabdioph  36859  monotoddzz  37027  aomclem2  37144  refsumcn  38711  refsum2cnlem1  38718  fvmpt2bd  38859  wessf1ornlem  38880  fompt  38888  projf1o  38895  choicefi  38901  axccdom  38925  fvmpt4  38956  feqresmpt2  38971  fsumsermpt  39247  fmuldfeqlem1  39250  fmuldfeq  39251  climneg  39278  climdivf  39280  mullimc  39284  idlimc  39294  sumnnodd  39298  neglimc  39315  addlimc  39316  0ellimcdiv  39317  climfveqmpt2  39361  climeqmpt  39365  limsupequzmptlem  39396  cncfmptssg  39418  cncfshift  39422  icccncfext  39435  cncfiooicclem1  39441  fprodsubrecnncnvlem  39456  fprodaddrecnncnvlem  39458  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnmptdivc  39490  dvnmul  39495  dvnprodlem2  39499  itgsin0pilem1  39502  ibliccsinexp  39503  itgsinexplem1  39506  itgsinexp  39507  ditgeqiooicc  39513  itgsubsticclem  39528  itgioocnicc  39530  stoweidlem2  39556  stoweidlem11  39565  stoweidlem12  39566  stoweidlem16  39570  stoweidlem17  39571  stoweidlem18  39572  stoweidlem19  39573  stoweidlem20  39574  stoweidlem21  39575  stoweidlem22  39576  stoweidlem23  39577  stoweidlem27  39581  stoweidlem31  39585  stoweidlem34  39588  stoweidlem36  39590  stoweidlem40  39594  stoweidlem41  39595  stoweidlem42  39596  stoweidlem48  39602  stoweidlem55  39609  stoweidlem59  39613  stoweidlem62  39616  stirlinglem3  39630  stirlinglem8  39635  stirlinglem14  39641  stirlinglem15  39642  stirlingr  39644  dirkeritg  39656  dirkercncflem2  39658  fourierdlem14  39675  fourierdlem31  39692  fourierdlem41  39702  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem51  39711  fourierdlem56  39716  fourierdlem60  39720  fourierdlem61  39721  fourierdlem66  39726  fourierdlem70  39730  fourierdlem71  39731  fourierdlem73  39733  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem77  39737  fourierdlem78  39738  fourierdlem81  39741  fourierdlem83  39743  fourierdlem84  39744  fourierdlem85  39745  fourierdlem87  39747  fourierdlem88  39748  fourierdlem89  39749  fourierdlem91  39751  fourierdlem92  39752  fourierdlem93  39753  fourierdlem95  39755  fourierdlem97  39757  fourierdlem101  39761  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  fourierdlem112  39772  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  elaa2lem  39787  etransclem4  39792  etransclem13  39801  etransclem35  39823  etransclem46  39834  etransclem48  39836  sge0revalmpt  39932  sge0fsummpt  39944  sge0iunmptlemfi  39967  sge0iunmptlemre  39969  sge0ltfirpmpt2  39980  sge0fsummptf  39990  nnfoctbdjlem  40009  iundjiun  40014  meaiunlelem  40022  meaiuninclem  40034  omeiunlempt  40071  carageniuncllem2  40073  caratheodorylem2  40078  0ome  40080  isomenndlem  40081  hoicvr  40099  hoicvrrex  40107  ovn0lem  40116  ovnsubaddlem1  40121  hoidmvlelem2  40147  hoidmvlelem3  40148  ovnhoilem2  40153  hoicoto2  40156  hoi2toco  40158  ovnlecvr2  40161  ovncvr2  40162  ovnsubadd2lem  40196  ovolval5lem2  40204  ovnovollem1  40207  ovnovollem2  40208  vonioolem1  40231  smfaddlem1  40308  smflimlem2  40317  smflimmpt  40353  smfsupmpt  40358  smfinfmpt  40362  smflimsuplem2  40364  smflimsuplem4  40366  smflimsuplem5  40367  smflimsupmpt  40372  aacllem  41880
 Copyright terms: Public domain W3C validator