Theorem funmpt 6604

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 6603	. 2 ⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		df-mpt 5226	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	2	funeqi 6587	. 2 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)})
4	1, 3	mpbir 231	1 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5205   ↦ cmpt 5225  Fun wfun 6555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-fun 6563

This theorem is referenced by:  funmpt2  6605  resfunexg  7235  mptexg  7241  mptexgf  7242  mptexw  7977  brtpos2  8257  tposfun  8267  mptfi  9391  fsuppssov1  9424  sniffsupp  9440  cantnfrescl  9716  cantnflem1  9729  r0weon  10052  axcc2lem  10476  mptct  10578  negfi  12217  mptnn0fsupp  14038  ccatalpha  14631  mreacs  17701  acsfn  17702  isofval  17801  lubfun  18397  glbfun  18410  acsficl2d  18597  gsum2dlem2  19989  gsum2d  19990  dprdfinv  20039  dprdfadd  20040  dmdprdsplitlem  20057  dpjidcl  20078  mptscmfsupp0  20925  pjpm  21728  frlmphllem  21800  uvcff  21811  uvcresum  21813  psrass1lem  21952  psrlidm  21982  psrridm  21983  psrass1  21984  psrass23l  21987  psrcom  21988  psrass23  21989  mplsubrg  22025  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  mplbas2  22060  evlslem2  22103  evlslem6  22105  psdmplcl  22166  psdmul  22170  psropprmul  22239  coe1mul2  22272  evls1fpws  22373  oftpos  22458  pmatcollpw2lem  22783  tgrest  23167  cmpfi  23416  1stcrestlem  23460  ptcnplem  23629  xkoinjcn  23695  symgtgp  24114  eltsms  24141  rrxmval  25439  tdeglem4  26099  plypf1  26251  tayl0  26403  taylthlem1  26415  xrlimcnp  27011  nosupno  27748  noinfno  27763  abrexexd  32528  ofpreima  32675  fisuppov1  32692  mptiffisupp  32702  mptctf  32729  gsummptres2  33056  psgnfzto1stlem  33120  rmfsupp2  33242  elrspunidl  33456  elrspunsn  33457  locfinreflem  33839  measdivcstALTV  34226  sitgf  34349  imageval  35931  poimirlem30  37657  poimir  37660  evlsvvvallem2  42572  evlsvvval  42573  selvvvval  42595  evlselv  42597  mhphf  42607  choicefi  45205  rn1st  45280  fourierdlem80  46201  sge0tsms  46395  scmsuppss  48287  rmfsupp  48289  scmfsupp  48291  fdivval  48460