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

Theorem funmpt 5575
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 5574 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4422 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5559 . 2  |-  ( Fun  ( x  e.  A  |->  B )  <->  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) } )
41, 3mpbir 212 1  |-  Fun  (
x  e.  A  |->  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437    e. wcel 1872   {copab 4419    |-> cmpt 4420   Fun wfun 5533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-fun 5541
This theorem is referenced by:  funmpt2  5576  fmptco  6010  resfunexg  6084  mptexg  6089  brtpos2  6929  tposfun  6939  mptfi  7821  sniffsupp  7871  cantnfrescl  8128  cantnflem1  8141  r0weon  8390  axcc2lem  8812  negfi  10500  mptnn0fsupp  12154  mreacs  15502  acsfn  15503  isofval  15600  lubfun  16164  glbfun  16177  acsficl2d  16360  pmtrsn  17098  gsum2dlem2  17541  gsum2d  17542  dprdfinv  17590  dprdfadd  17591  dmdprdsplitlem  17608  dpjidcl  17629  mptscmfsupp0  18091  00lsp  18142  psrass1lem  18539  psrlidm  18565  psrridm  18566  psrass1  18567  psrass23l  18570  psrcom  18571  psrass23  18572  mplsubrg  18602  mplmon  18625  mplmonmul  18626  mplcoe1  18627  mplcoe5  18630  mplbas2  18632  evlslem2  18673  evlslem6  18674  psropprmul  18769  coe1mul2  18800  ply1coeOLD  18828  pjpm  19208  frlmphllem  19275  frlmphl  19276  uvcff  19286  uvcresum  19288  oftpos  19414  pmatcollpw2lem  19738  tgrest  20112  cmpfi  20360  1stcrestlem  20404  ptcnplem  20573  xkoinjcn  20639  symgtgp  21053  eltsms  21084  rrxmval  22296  tdeglem4  22946  plypf1  23103  tayl0  23254  taylthlem1  23265  xrlimcnp  23831  abrexexd  28081  mptexgf  28166  fmptcof2  28200  ofpreima  28209  funcnvmptOLD  28211  mptct  28247  mptctf  28250  psgnfzto1stlem  28560  locfinreflem  28614  measdivcstOLD  28993  sxbrsigalem0  29040  sitgf  29127  imageval  30641  poimirlem30  31877  poimir  31880  fourierdlem80  37933  sge0tsms  38073  scmsuppss  39750  rmfsupp  39752  scmfsupp  39756  fdivval  39943
  Copyright terms: Public domain W3C validator