MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funmpt Structured version   Unicode version

Theorem funmpt 5622
Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
Assertion
Ref Expression
funmpt  |-  Fun  (
x  e.  A  |->  B )

Proof of Theorem funmpt
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 funopab4 5621 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4507 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5606 . 2  |-  ( Fun  ( x  e.  A  |->  B )  <->  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) } )
41, 3mpbir 209 1  |-  Fun  (
x  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1379    e. wcel 1767   {copab 4504    |-> cmpt 4505   Fun wfun 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-fun 5588
This theorem is referenced by:  funmpt2  5623  fmptco  6052  resfunexg  6124  mptexg  6128  brtpos2  6958  tposfun  6968  mptfi  7815  sniffsupp  7865  cantnfrescl  8091  cantnflem1d  8103  cantnflem1  8104  r0weon  8386  axcc2lem  8812  mptnn0fsupp  12067  mreacs  14909  acsfn  14910  isoval  15016  lubfun  15463  glbfun  15476  acsficl2d  15659  pmtrsn  16340  gsum2dlem2  16789  gsum2d  16790  dprdfinv  16849  dprdfadd  16850  dmdprdsplitlem  16874  dpjidcl  16897  mptscmfsupp0  17359  00lsp  17410  psrass1lem  17800  psrlidm  17827  psrridm  17829  psrass1  17831  psrdi  17832  psrdir  17833  psrass23l  17834  psrcom  17835  psrass23  17836  mplsubrg  17873  mplmon  17896  mplmonmul  17897  mplcoe1  17898  mplcoe5  17902  mplbas2  17905  evlslem2  17951  evlslem6  17952  psropprmul  18050  coe1mul2  18081  ply1coeOLD  18109  pjpm  18506  frlmphllem  18578  frlmphl  18579  uvcff  18589  uvcresum  18591  oftpos  18721  pmatcollpw2lem  19045  tgrest  19426  cmpfi  19674  1stcrestlem  19719  ptcnplem  19857  xkoinjcn  19923  symgtgp  20335  eltsms  20366  rrxmval  21567  tdeglem4  22193  plypf1  22344  tayl0  22491  taylthlem1  22502  xrlimcnp  23026  abrexexd  27081  fmptcof2  27174  ofpreima  27179  funcnvmptOLD  27181  mptct  27213  mptctf  27216  measdivcstOLD  27835  sxbrsigalem0  27882  sitgf  27929  imageval  29157  fourierdlem80  31487  scmsuppss  32038  rmfsupp  32040  scmfsupp  32044
  Copyright terms: Public domain W3C validator