Theorem funmpt 5840

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

Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {copab 4642   ↦ cmpt 4643  Fun wfun 5798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-fun 5806

This theorem is referenced by:  funmpt2  5841  resfunexg  6384  mptexg  6389  brtpos2  7245  tposfun  7255  mptfi  8148  sniffsupp  8198  cantnfrescl  8456  cantnflem1  8469  r0weon  8718  axcc2lem  9141  negfi  10850  mptnn0fsupp  12659  ccatalpha  13228  mreacs  16142  acsfn  16143  isofval  16240  lubfun  16803  glbfun  16816  acsficl2d  16999  pmtrsn  17762  gsum2dlem2  18193  gsum2d  18194  dprdfinv  18241  dprdfadd  18242  dmdprdsplitlem  18259  dpjidcl  18280  mptscmfsupp0  18751  00lsp  18802  psrass1lem  19198  psrlidm  19224  psrridm  19225  psrass1  19226  psrass23l  19229  psrcom  19230  psrass23  19231  mplsubrg  19261  mplmon  19284  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  mplbas2  19291  evlslem2  19333  evlslem6  19334  psropprmul  19429  coe1mul2  19460  pjpm  19871  frlmphllem  19938  frlmphl  19939  uvcff  19949  uvcresum  19951  oftpos  20077  pmatcollpw2lem  20401  tgrest  20773  cmpfi  21021  1stcrestlem  21065  ptcnplem  21234  xkoinjcn  21300  symgtgp  21715  eltsms  21746  rrxmval  22996  tdeglem4  23624  plypf1  23772  tayl0  23920  taylthlem1  23931  xrlimcnp  24495  abrexexd  28731  mptexgf  28809  fmptcof2  28839  ofpreima  28848  funcnvmptOLD  28850  mptct  28880  mptctf  28883  psgnfzto1stlem  29181  locfinreflem  29235  measdivcstOLD  29614  sxbrsigalem0  29660  sitgf  29736  imageval  31207  poimirlem30  32609  poimir  32612  choicefi  38387  fourierdlem80  39079  sge0tsms  39273  scmsuppss  41947  rmfsupp  41949  scmfsupp  41953  fdivval  42131