Theorem funmpt 6605

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.

Step	Hyp	Ref	Expression
1		funopab4 6604	. 2 ⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		df-mpt 5231	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	2	funeqi 6588	. 2 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)})
4	1, 3	mpbir 231	1 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {copab 5209   ↦ cmpt 5230  Fun wfun 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-fun 6564

This theorem is referenced by:  funmpt2  6606  resfunexg  7234  mptexg  7240  mptexgf  7241  mptexw  7975  brtpos2  8255  tposfun  8265  mptfi  9388  fsuppssov1  9421  sniffsupp  9437  cantnfrescl  9713  cantnflem1  9726  r0weon  10049  axcc2lem  10473  mptct  10575  negfi  12214  mptnn0fsupp  14034  ccatalpha  14627  mreacs  17702  acsfn  17703  isofval  17804  lubfun  18409  glbfun  18422  acsficl2d  18609  gsum2dlem2  20003  gsum2d  20004  dprdfinv  20053  dprdfadd  20054  dmdprdsplitlem  20071  dpjidcl  20092  mptscmfsupp0  20941  pjpm  21745  frlmphllem  21817  uvcff  21828  uvcresum  21830  psrass1lem  21969  psrlidm  21999  psrridm  22000  psrass1  22001  psrass23l  22004  psrcom  22005  psrass23  22006  mplsubrg  22042  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  mplbas2  22077  evlslem2  22120  evlslem6  22122  psdmplcl  22183  psdmul  22187  psropprmul  22254  coe1mul2  22287  evls1fpws  22388  oftpos  22473  pmatcollpw2lem  22798  tgrest  23182  cmpfi  23431  1stcrestlem  23475  ptcnplem  23644  xkoinjcn  23710  symgtgp  24129  eltsms  24156  rrxmval  25452  tdeglem4  26113  plypf1  26265  tayl0  26417  taylthlem1  26429  xrlimcnp  27025  nosupno  27762  noinfno  27777  abrexexd  32536  ofpreima  32681  fisuppov1  32697  mptiffisupp  32707  mptctf  32734  gsummptres2  33038  psgnfzto1stlem  33102  rmfsupp2  33227  elrspunidl  33435  elrspunsn  33436  locfinreflem  33800  measdivcstALTV  34205  sitgf  34328  imageval  35911  poimirlem30  37636  poimir  37639  evlsvvvallem2  42548  evlsvvval  42549  selvvvval  42571  evlselv  42573  mhphf  42583  choicefi  45142  rn1st  45218  fourierdlem80  46141  sge0tsms  46335  scmsuppss  48215  rmfsupp  48217  scmfsupp  48219  fdivval  48388