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

Theorem fvmpt2 6185
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 6184 . 2 (𝑥𝐴 → (𝐹𝑥) = ( I ‘𝐵))
3 fvi 6150 . 2 (𝐵𝐶 → ( I ‘𝐵) = 𝐵)
42, 3sylan9eq 2663 1 ((𝑥𝐴𝐵𝐶) → (𝐹𝑥) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  cmpt 4637   I cid 4938  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fv 5798
This theorem is referenced by:  fvmptss  6186  fvmpt2d  6187  fvmptdf  6189  mpteqb  6192  fvmptt  6193  fvmptf  6194  fnmptfvd  6213  ralrnmpt  6261  fmptco  6288  f1mpt  6397  offval2  6789  ofrfval2  6790  mptelixpg  7808  dom2lem  7858  mapxpen  7988  xpmapenlem  7989  cnfcom3clem  8462  tcvalg  8474  rankf  8517  infxpenc2lem2  8703  dfac8clem  8715  acni2  8729  acnlem  8731  fin23lem32  9026  axcc2lem  9118  axcc3  9120  domtriomlem  9124  ac6num  9161  konigthlem  9246  rpnnen1lem1  11647  rpnnen1lem3  11648  rpnnen1lem5  11650  rpnnen1lem1OLD  11653  rpnnen1lem3OLD  11654  rpnnen1lem5OLD  11656  seqof  12675  seqof2  12676  rlim2  14021  ello1mpt  14046  o1compt  14112  sumrblem  14235  fsumcvg  14236  summolem2a  14239  fsum  14244  fsumcvg2  14251  fsumadd  14263  isummulc2  14281  fsummulc2  14304  fsumrelem  14326  prodrblem  14444  fprodcvg  14445  prodmolem2a  14449  zprod  14452  fprod  14456  fprodmul  14475  fproddiv  14476  iserodd  15324  prmrec  15410  prdsbas3  15910  prdsdsval2  15913  invfuc  16403  yonedalem4c  16686  gsumconst  18103  prdsgsum  18146  gsumdixp  18378  evlslem4  19275  elptr2  21129  ptunimpt  21150  ptcldmpt  21169  ptclsg  21170  txcnp  21175  ptcnplem  21176  cnmpt11  21218  cnmpt1t  21220  cnmptk2  21241  xkocnv  21369  flfcnp2  21563  ustn0  21776  utopsnneiplem  21803  ucnima  21837  iccpnfcnv  22482  ovolctb  22982  ovoliunlem1  22994  ovoliun2  22998  ovolshftlem1  23001  ovolscalem1  23005  voliun  23046  ioombl1lem3  23052  ioombl1lem4  23053  uniioombllem2  23074  mbfeqalem  23132  mbfpos  23141  mbfposr  23142  mbfposb  23143  mbfsup  23154  mbfinf  23155  mbflim  23158  i1fposd  23197  itg1climres  23204  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  itg2split  23239  itg2mono  23243  itg2cnlem1  23251  isibl2  23256  itgmpt  23272  itgeqa  23303  itggt0  23331  itgcn  23332  limcmpt  23370  dvlipcn  23478  lhop2  23499  dvfsumabs  23507  itgparts  23531  itgsubstlem  23532  itgsubst  23533  elplyd  23679  coeeulem  23701  coeeq2  23719  dvply1  23760  plyremlem  23780  ulmss  23872  ulmdvlem1  23875  mtest  23879  itgulm2  23884  radcnvlem1  23888  pserulm  23897  leibpi  24386  rlimcnp  24409  o1cxp  24418  lgamgulmlem2  24473  lgamgulmlem6  24477  lgamgulm2  24479  sqff1o  24625  lgseisenlem2  24818  dchrvmasumlem1  24901  frgrancvvdeqlem6  26328  ubthlem1  26916  cnlnadjlem5  28120  xppreima2  28636  abfmpunirn  28638  aciunf1lem  28650  fpwrelmap  28702  fimaproj  29034  xrmulc1cn  29110  esumpcvgval  29273  esumsup  29284  voliune  29425  eulerpartgbij  29567  signsplypnf  29759  iscvm  30301  mclsrcl  30518  f1omptsnlem  32155  matunitlindflem2  32372  itg2addnclem  32427  itggt0cn  32448  ftc1anclem5  32455  elrfirn2  36073  eq0rabdioph  36154  monotoddzz  36322  aomclem2  36439  refsumcn  38008  refsum2cnlem1  38015  fvmpt2bd  38141  wessf1ornlem  38162  fompt  38170  projf1o  38177  choicefi  38183  axccdom  38207  fsumsermpt  38443  fmuldfeqlem1  38446  fmuldfeq  38447  climneg  38474  climdivf  38476  mullimc  38480  idlimc  38490  sumnnodd  38494  neglimc  38511  addlimc  38512  0ellimcdiv  38513  cncfmptssg  38552  cncfshift  38556  icccncfext  38570  cncfiooicclem1  38576  fprodsubrecnncnvlem  38591  fprodaddrecnncnvlem  38593  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnmptdivc  38625  dvnmul  38630  dvnprodlem2  38634  itgsin0pilem1  38638  ibliccsinexp  38639  itgsinexplem1  38642  itgsinexp  38643  ditgeqiooicc  38649  itgsubsticclem  38664  itgioocnicc  38666  stoweidlem2  38692  stoweidlem11  38701  stoweidlem12  38702  stoweidlem16  38706  stoweidlem17  38707  stoweidlem18  38708  stoweidlem19  38709  stoweidlem20  38710  stoweidlem21  38711  stoweidlem22  38712  stoweidlem23  38713  stoweidlem27  38717  stoweidlem31  38721  stoweidlem34  38724  stoweidlem36  38726  stoweidlem40  38730  stoweidlem41  38731  stoweidlem42  38732  stoweidlem48  38738  stoweidlem55  38745  stoweidlem59  38749  stoweidlem62  38752  stirlinglem3  38766  stirlinglem8  38771  stirlinglem14  38777  stirlinglem15  38778  stirlingr  38780  dirkeritg  38792  dirkercncflem2  38794  fourierdlem14  38811  fourierdlem31  38828  fourierdlem41  38838  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem51  38847  fourierdlem56  38852  fourierdlem60  38856  fourierdlem61  38857  fourierdlem66  38862  fourierdlem70  38866  fourierdlem71  38867  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem77  38873  fourierdlem78  38874  fourierdlem81  38877  fourierdlem83  38879  fourierdlem84  38880  fourierdlem85  38881  fourierdlem87  38883  fourierdlem88  38884  fourierdlem89  38885  fourierdlem91  38887  fourierdlem92  38888  fourierdlem93  38889  fourierdlem95  38891  fourierdlem97  38893  fourierdlem101  38897  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem112  38908  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  elaa2lem  38923  etransclem4  38928  etransclem13  38937  etransclem35  38959  etransclem46  38970  etransclem48  38972  sge0revalmpt  39068  sge0fsummpt  39080  sge0iunmptlemfi  39103  sge0iunmptlemre  39105  sge0ltfirpmpt2  39116  sge0fsummptf  39126  nnfoctbdjlem  39145  iundjiun  39150  meaiunlelem  39158  meaiuninclem  39170  omeiunlempt  39207  carageniuncllem2  39209  caratheodorylem2  39214  0ome  39216  isomenndlem  39217  hoicvr  39235  hoicvrrex  39243  ovn0lem  39252  ovnsubaddlem1  39257  hoidmvlelem2  39283  hoidmvlelem3  39284  ovnhoilem2  39289  hoicoto2  39292  hoi2toco  39294  ovnlecvr2  39297  ovncvr2  39298  ovnsubadd2lem  39332  ovolval5lem2  39340  ovnovollem1  39343  ovnovollem2  39344  vonioolem1  39368  smfaddlem1  39446  smflimlem2  39455  frgrncvvdeqlem6  41469  aacllem  42312
  Copyright terms: Public domain W3C validator