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

Theorem funmpt 5449
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 5448 . 2  |-  Fun  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
2 df-mpt 4347 . . 3  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
32funeqi 5433 . 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 1369    e. wcel 1756   {copab 4344    e. cmpt 4345   Fun wfun 5407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-fun 5415
This theorem is referenced by:  funmpt2  5450  fmptco  5871  resfunexg  5938  mptexg  5942  brtpos2  6746  tposfun  6756  mptfi  7602  sniffsupp  7651  cantnfrescl  7876  cantnflem1d  7888  cantnflem1  7889  r0weon  8171  axcc2lem  8597  mreacs  14588  acsfn  14589  isoval  14695  lubfun  15142  glbfun  15155  acsficl2d  15338  gsum2dlem2  16450  gsum2d  16451  dprdfinv  16497  dprdfadd  16498  dmdprdsplitlem  16522  dpjidcl  16545  mptscmfsuppd  16989  00lsp  17039  psrass1lem  17424  psrlidm  17451  psrridm  17453  psrass1  17455  psrdi  17456  psrdir  17457  psrcom  17458  psrass23  17459  mplsubrg  17496  mplmon  17519  mplmonmul  17520  mplcoe1  17521  mplcoe2  17524  mplbas2  17526  evlslem2  17572  evlslem6  17573  psropprmul  17668  coe1mul2  17698  ply1coeOLD  17722  pjpm  18108  frlmphllem  18180  frlmphl  18181  uvcff  18191  uvcresum  18193  oftpos  18308  tgrest  18738  cmpfi  18986  1stcrestlem  19031  ptcnplem  19169  xkoinjcn  19235  symgtgp  19647  eltsms  19678  rrxmval  20879  tdeglem4  21504  plypf1  21655  tayl0  21802  taylthlem1  21813  xrlimcnp  22337  abrexexd  25841  fmptcof2  25930  ofpreima  25935  funcnvmptOLD  25937  mptct  25969  mptctf  25972  measdivcstOLD  26590  sxbrsigalem0  26638  sitgf  26685  imageval  27912  pmtrsn  30721  scmsuppss  30736  rmfsupp  30738  scmfsupp  30742  psrass23l  30763  pmatcollpw1lem4  30817  pmatcollpw2lem  30820
  Copyright terms: Public domain W3C validator