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

Theorem funmpt 6536
Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
Assertion
Ref Expression
funmpt Fun (𝑥𝐴𝐵)

Proof of Theorem funmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 funopab4 6535 . 2 Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
2 df-mpt 5187 . . 3 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
32funeqi 6519 . 2 (Fun (𝑥𝐴𝐵) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)})
41, 3mpbir 230 1 Fun (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  {copab 5165  cmpt 5186  Fun wfun 6487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6495
This theorem is referenced by:  funmpt2  6537  resfunexg  7161  mptexg  7167  mptexgf  7168  mptexw  7881  brtpos2  8159  tposfun  8169  mptfi  9291  sniffsupp  9332  cantnfrescl  9608  cantnflem1  9621  r0weon  9944  axcc2lem  10368  mptct  10470  negfi  12100  mptnn0fsupp  13894  ccatalpha  14473  mreacs  17530  acsfn  17531  isofval  17632  lubfun  18233  glbfun  18246  acsficl2d  18433  gsum2dlem2  19739  gsum2d  19740  dprdfinv  19789  dprdfadd  19790  dmdprdsplitlem  19807  dpjidcl  19828  mptscmfsupp0  20372  pjpm  21099  frlmphllem  21171  frlmphl  21172  uvcff  21182  uvcresum  21184  psrass1lemOLD  21327  psrass1lem  21330  psrlidm  21356  psrridm  21357  psrass1  21358  psrass23l  21361  psrcom  21362  psrass23  21363  mplsubrg  21395  mplmon  21420  mplmonmul  21421  mplcoe1  21422  mplcoe5  21425  mplbas2  21427  evlslem2  21473  evlslem6  21475  psropprmul  21593  coe1mul2  21624  oftpos  21785  pmatcollpw2lem  22110  tgrest  22494  cmpfi  22743  1stcrestlem  22787  ptcnplem  22956  xkoinjcn  23022  symgtgp  23441  eltsms  23468  rrxmval  24753  tdeglem4  25408  tdeglem4OLD  25409  plypf1  25557  tayl0  25705  taylthlem1  25716  xrlimcnp  26302  nosupno  27035  noinfno  27050  abrexexd  31321  ofpreima  31467  mptctf  31517  gsummptres2  31778  psgnfzto1stlem  31832  rmfsupp2  31958  elrspunidl  32082  evls1fpws  32149  locfinreflem  32290  measdivcstALTV  32693  sitgf  32816  imageval  34482  poimirlem30  36075  poimir  36078  evlsbagval  40699  mhphf  40709  choicefi  43357  rn1st  43439  fourierdlem80  44359  sge0tsms  44553  scmsuppss  46380  rmfsupp  46382  scmfsupp  46386  fdivval  46557
  Copyright terms: Public domain W3C validator