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

Theorem funmpt 5561
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 5560 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4459 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5545 . 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 1370    e. wcel 1758   {copab 4456    |-> cmpt 4457   Fun wfun 5519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-fun 5527
This theorem is referenced by:  funmpt2  5562  fmptco  5984  resfunexg  6051  mptexg  6055  brtpos2  6860  tposfun  6870  mptfi  7720  sniffsupp  7769  cantnfrescl  7994  cantnflem1d  8006  cantnflem1  8007  r0weon  8289  axcc2lem  8715  mreacs  14714  acsfn  14715  isoval  14821  lubfun  15268  glbfun  15281  acsficl2d  15464  pmtrsn  16143  gsum2dlem2  16583  gsum2d  16584  dprdfinv  16630  dprdfadd  16631  dmdprdsplitlem  16655  dpjidcl  16678  mptscmfsupp0  17133  00lsp  17184  psrass1lem  17569  psrlidm  17596  psrridm  17598  psrass1  17600  psrdi  17601  psrdir  17602  psrass23l  17603  psrcom  17604  psrass23  17605  mplsubrg  17642  mplmon  17665  mplmonmul  17666  mplcoe1  17667  mplcoe5  17671  mplbas2  17674  evlslem2  17720  evlslem6  17721  psropprmul  17815  coe1mul2  17845  ply1coeOLD  17871  pjpm  18257  frlmphllem  18329  frlmphl  18330  uvcff  18340  uvcresum  18342  oftpos  18459  tgrest  18894  cmpfi  19142  1stcrestlem  19187  ptcnplem  19325  xkoinjcn  19391  symgtgp  19803  eltsms  19834  rrxmval  21035  tdeglem4  21661  plypf1  21812  tayl0  21959  taylthlem1  21970  xrlimcnp  22494  abrexexd  26041  fmptcof2  26129  ofpreima  26134  funcnvmptOLD  26136  mptct  26168  mptctf  26171  measdivcstOLD  26782  sxbrsigalem0  26829  sitgf  26876  imageval  28104  scmsuppss  30932  rmfsupp  30935  scmfsupp  30939  mptnn0fsupp  30949  pmatcollpw2lem  31250
  Copyright terms: Public domain W3C validator