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

Theorem funmpt 5605
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 5604 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4455 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5589 . 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 367    = wceq 1405    e. wcel 1842   {copab 4452    |-> cmpt 4453   Fun wfun 5563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-fun 5571
This theorem is referenced by:  funmpt2  5606  fmptco  6043  resfunexg  6118  mptexg  6123  brtpos2  6964  tposfun  6974  mptfi  7853  sniffsupp  7903  cantnfrescl  8127  cantnflem1  8140  r0weon  8422  axcc2lem  8848  mptnn0fsupp  12147  mreacs  15272  acsfn  15273  isofval  15370  lubfun  15934  glbfun  15947  acsficl2d  16130  pmtrsn  16868  gsum2dlem2  17319  gsum2d  17320  dprdfinv  17379  dprdfadd  17380  dmdprdsplitlem  17404  dpjidcl  17427  mptscmfsupp0  17896  00lsp  17947  psrass1lem  18349  psrlidm  18376  psrridm  18378  psrass1  18380  psrass23l  18383  psrcom  18384  psrass23  18385  mplsubrg  18422  mplmon  18445  mplmonmul  18446  mplcoe1  18447  mplcoe5  18451  mplbas2  18454  evlslem2  18500  evlslem6  18501  psropprmul  18599  coe1mul2  18630  ply1coeOLD  18658  pjpm  19037  frlmphllem  19107  frlmphl  19108  uvcff  19118  uvcresum  19120  oftpos  19246  pmatcollpw2lem  19570  tgrest  19953  cmpfi  20201  1stcrestlem  20245  ptcnplem  20414  xkoinjcn  20480  symgtgp  20892  eltsms  20923  rrxmval  22124  tdeglem4  22750  plypf1  22901  tayl0  23049  taylthlem1  23060  xrlimcnp  23624  abrexexd  27822  mptexgf  27908  fmptcof2  27941  ofpreima  27950  funcnvmptOLD  27952  mptct  27987  mptctf  27990  locfinreflem  28296  measdivcstOLD  28672  sxbrsigalem0  28719  sitgf  28795  imageval  30268  fourierdlem80  37337  scmsuppss  38476  rmfsupp  38478  scmfsupp  38482  fdivval  38670
  Copyright terms: Public domain W3C validator