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

Theorem fvmpt2 6445
 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 6444 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6409 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2806 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624   ∈ wcel 2131   ↦ cmpt 4873   I cid 5165  ‘cfv 6041 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fv 6049 This theorem is referenced by:  fvmptss  6446  fvmpt2d  6447  fvmptd3f  6449  mpteqb  6453  fvmptt  6454  fvmptf  6455  fnmptfvd  6475  ralrnmpt  6523  fmptco  6551  f1mpt  6673  offval2  7071  ofrfval2  7072  mptelixpg  8103  dom2lem  8153  mapxpen  8283  xpmapenlem  8284  cnfcom3clem  8767  tcvalg  8779  rankf  8822  infxpenc2lem2  9025  dfac8clem  9037  acni2  9051  acnlem  9053  fin23lem32  9350  axcc2lem  9442  axcc3  9444  domtriomlem  9448  ac6num  9485  konigthlem  9574  rpnnen1lem1  12000  rpnnen1lem3  12001  rpnnen1lem5  12003  rpnnen1lem1OLD  12006  rpnnen1lem3OLD  12007  rpnnen1lem5OLD  12009  seqof  13044  seqof2  13045  rlim2  14418  ello1mpt  14443  o1compt  14509  sumrblem  14633  fsumcvg  14634  summolem2a  14637  fsum  14642  fsumcvg2  14649  fsumadd  14661  isummulc2  14684  fsummulc2  14707  fsumrelem  14730  prodrblem  14850  fprodcvg  14851  prodmolem2a  14855  zprod  14858  fprod  14862  fprodmul  14881  fproddiv  14882  iserodd  15734  prmrec  15820  prdsbas3  16335  prdsdsval2  16338  invfuc  16827  yonedalem4c  17110  gsumconst  18526  prdsgsum  18569  gsumdixp  18801  evlslem4  19702  elptr2  21571  ptunimpt  21592  ptcldmpt  21611  ptclsg  21612  txcnp  21617  ptcnplem  21618  cnmpt11  21660  cnmpt1t  21662  cnmptk2  21683  xkocnv  21811  flfcnp2  22004  ustn0  22217  utopsnneiplem  22244  ucnima  22278  iccpnfcnv  22936  ovolctb  23450  ovoliunlem1  23462  ovoliun2  23466  ovolshftlem1  23469  ovolscalem1  23473  voliun  23514  ioombl1lem3  23520  ioombl1lem4  23521  uniioombllem2  23543  mbfeqalem  23600  mbfpos  23609  mbfposr  23610  mbfposb  23611  mbfsup  23622  mbfinf  23623  mbflim  23626  i1fposd  23665  itg1climres  23672  mbfi1fseqlem4  23676  mbfi1fseqlem5  23677  mbfi1fseqlem6  23678  itg2split  23707  itg2mono  23711  itg2cnlem1  23719  isibl2  23724  itgmpt  23740  itgeqa  23771  itggt0  23799  itgcn  23800  limcmpt  23838  dvlipcn  23948  lhop2  23969  dvfsumabs  23977  itgparts  24001  itgsubstlem  24002  itgsubst  24003  elplyd  24149  coeeulem  24171  coeeq2  24189  dvply1  24230  plyremlem  24250  ulmss  24342  ulmdvlem1  24345  mtest  24349  itgulm2  24354  radcnvlem1  24358  pserulm  24367  leibpi  24860  rlimcnp  24883  o1cxp  24892  lgamgulmlem2  24947  lgamgulmlem6  24951  lgamgulm2  24953  sqff1o  25099  lgseisenlem2  25292  dchrvmasumlem1  25375  frgrncvvdeqlem5  27449  ubthlem1  28027  cnlnadjlem5  29231  xppreima2  29751  abfmpunirn  29753  aciunf1lem  29763  fpwrelmap  29809  fimaproj  30201  xrmulc1cn  30277  esumpcvgval  30441  esumsup  30452  voliune  30593  eulerpartgbij  30735  signsplypnf  30928  iscvm  31540  mclsrcl  31757  f1omptsnlem  33486  matunitlindflem2  33711  itg2addnclem  33766  itggt0cn  33787  ftc1anclem5  33794  elrfirn2  37753  eq0rabdioph  37834  monotoddzz  38002  aomclem2  38119  refsumcn  39680  refsum2cnlem1  39687  fvmpt2bd  39841  wessf1ornlem  39862  fompt  39870  projf1o  39877  choicefi  39883  axccdom  39907  fvmpt4  39937  fsumsermpt  40306  fmuldfeqlem1  40309  fmuldfeq  40310  climneg  40337  climdivf  40339  mullimc  40343  idlimc  40353  sumnnodd  40357  neglimc  40374  addlimc  40375  0ellimcdiv  40376  climfveqmpt2  40420  climeqmpt  40424  limsupequzmptlem  40455  liminfvalxr  40510  xlimmnfmpt  40564  xlimpnfmpt  40565  cncfmptssg  40578  cncfshift  40582  icccncfext  40595  cncfiooicclem1  40601  fprodsubrecnncnvlem  40616  fprodaddrecnncnvlem  40618  ioodvbdlimc1lem2  40642  ioodvbdlimc2lem  40644  dvnmptdivc  40648  dvnmul  40653  dvnprodlem2  40657  itgsin0pilem1  40660  ibliccsinexp  40661  itgsinexplem1  40664  itgsinexp  40665  ditgeqiooicc  40671  itgsubsticclem  40686  itgioocnicc  40688  stoweidlem2  40714  stoweidlem11  40723  stoweidlem12  40724  stoweidlem16  40728  stoweidlem17  40729  stoweidlem18  40730  stoweidlem19  40731  stoweidlem20  40732  stoweidlem21  40733  stoweidlem22  40734  stoweidlem23  40735  stoweidlem27  40739  stoweidlem31  40743  stoweidlem34  40746  stoweidlem36  40748  stoweidlem40  40752  stoweidlem41  40753  stoweidlem42  40754  stoweidlem48  40760  stoweidlem55  40767  stoweidlem59  40771  stoweidlem62  40774  stirlinglem3  40788  stirlinglem8  40793  stirlinglem14  40799  stirlinglem15  40800  stirlingr  40802  dirkeritg  40814  dirkercncflem2  40816  fourierdlem14  40833  fourierdlem31  40850  fourierdlem41  40860  fourierdlem48  40866  fourierdlem49  40867  fourierdlem50  40868  fourierdlem51  40869  fourierdlem56  40874  fourierdlem60  40878  fourierdlem61  40879  fourierdlem66  40884  fourierdlem70  40888  fourierdlem71  40889  fourierdlem73  40891  fourierdlem74  40892  fourierdlem75  40893  fourierdlem76  40894  fourierdlem77  40895  fourierdlem78  40896  fourierdlem81  40899  fourierdlem83  40901  fourierdlem84  40902  fourierdlem85  40903  fourierdlem87  40905  fourierdlem88  40906  fourierdlem89  40907  fourierdlem91  40909  fourierdlem92  40910  fourierdlem93  40911  fourierdlem95  40913  fourierdlem97  40915  fourierdlem101  40919  fourierdlem103  40921  fourierdlem104  40922  fourierdlem111  40929  fourierdlem112  40930  sqwvfoura  40940  sqwvfourb  40941  fouriersw  40943  elaa2lem  40945  etransclem4  40950  etransclem13  40959  etransclem35  40981  etransclem46  40992  etransclem48  40994  sge0revalmpt  41090  sge0fsummpt  41102  sge0iunmptlemfi  41125  sge0iunmptlemre  41127  sge0ltfirpmpt2  41138  sge0fsummptf  41148  nnfoctbdjlem  41167  iundjiun  41172  meaiunlelem  41180  meaiuninclem  41192  meaiuninc3v  41196  omeiunlempt  41232  carageniuncllem2  41234  caratheodorylem2  41239  0ome  41241  isomenndlem  41242  hoicvr  41260  hoicvrrex  41268  ovn0lem  41277  ovnsubaddlem1  41282  hoidmvlelem2  41308  hoidmvlelem3  41309  ovnhoilem2  41314  hoicoto2  41317  hoi2toco  41319  ovnlecvr2  41322  ovncvr2  41323  ovnsubadd2lem  41357  ovolval5lem2  41365  ovnovollem1  41368  ovnovollem2  41369  vonioolem1  41392  smfaddlem1  41469  smflimlem2  41478  smflimmpt  41514  smfsupmpt  41519  smfinfmpt  41523  smflimsuplem2  41525  smflimsuplem4  41527  smflimsuplem5  41528  smflimsupmpt  41533  smfliminfmpt  41536  aacllem  43052
 Copyright terms: Public domain W3C validator