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

Theorem funmpt 5442
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 5441 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4340 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5426 . 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 1362    e. wcel 1755   {copab 4337    e. cmpt 4338   Fun wfun 5400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-fun 5408
This theorem is referenced by:  funmpt2  5443  fmptco  5863  resfunexg  5930  mptexg  5934  brtpos2  6740  tposfun  6750  mptfi  7598  sniffsupp  7647  cantnfrescl  7872  cantnflem1d  7884  cantnflem1  7885  r0weon  8167  axcc2lem  8593  mreacs  14579  acsfn  14580  isoval  14686  lubfun  15133  glbfun  15146  acsficl2d  15329  gsum2dlem2  16436  gsum2d  16437  dprdfinv  16483  dprdfadd  16484  dmdprdsplitlem  16508  dpjidcl  16531  00lsp  16984  psrass1lem  17381  psrlidm  17408  psrridm  17410  psrass1  17412  psrdi  17413  psrdir  17414  psrcom  17415  psrass23  17416  mplsubrg  17453  mplmon  17476  mplmonmul  17477  mplcoe1  17478  mplcoe2  17481  mplbas2  17483  evlslem2  17525  psropprmul  17591  coe1mul2  17621  ply1coe  17643  pjpm  17975  frlmphllem  18047  frlmphl  18048  uvcff  18058  uvcresum  18060  oftpos  18175  tgrest  18605  cmpfi  18853  1stcrestlem  18898  ptcnplem  19036  xkoinjcn  19102  symgtgp  19514  eltsms  19545  rrxmval  20746  evlslem6  21364  tdeglem4  21414  plypf1  21565  tayl0  21712  taylthlem1  21723  xrlimcnp  22247  abrexexd  25714  fmptcof2  25803  ofpreima  25808  funcnvmptOLD  25810  mptct  25842  mptctf  25845  measdivcstOLD  26492  sxbrsigalem0  26540  sitgf  26581  imageval  27808  pmtrsn  30602  scmsuppss  30617  rmfsupp  30619  scmfsupp  30623  mptscmfsuppd  30626  psrass23l  30633
  Copyright terms: Public domain W3C validator