Theorem funmpt 6574

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

This proof depends on syntax axioms:   ∧ wa 400   = wceq 1569   ∈ wcel 2142  {copab 5172   ↦ cmpt 5191  Fun wfun 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-fun 6538

This theorem is used by:  funmpt2  6575  resfunexg  7213  mptexg  7219  mptexgf  7220  mptexw  7948  brtpos2  8226  tposfun  8236  mptfi  9306  fsuppssov1  9342  sniffsupp  9358  cantnfrescl  9643  cantnflem1  9656  r0weon  10003  axcc2lem  10426  mptct  10528  negfi  12170  mptnn0fsupp  14040  ccatalpha  14638  mreacs  17720  acsfn  17721  isofval  17820  lubfun  18412  glbfun  18425  acsficl2d  18614  gsum2dlem2  20047  gsum2d  20048  dprdfinv  20097  dprdfadd  20098  dmdprdsplitlem  20115  dpjidcl  20136  mptscmfsupp0  21059  pjpm  21869  frlmphllem  21941  uvcff  21952  uvcresum  21954  psrass1lem  22094  psrlidm  22122  psrridm  22123  psrass1  22124  psrass23l  22127  psrcom  22128  psrass23  22129  mplsubrg  22165  mplmon  22197  mplmonmul  22198  mplcoe1  22199  mplcoe5  22202  mplbas2  22204  evlslem2  22241  evlslem6  22243  evlsvvvallem2  22254  evlsvvval  22255  selvvvval  22304  psdmplcl  22336  psdmul  22340  psropprmul  22408  coe1mul2  22441  evls1fpws  22540  oftpos  22620  pmatcollpw2lem  22945  tgrest  23327  cmpfi  23576  1stcrestlem  23620  ptcnplem  23789  xkoinjcn  23855  symgtgp  24274  eltsms  24301  rrxmval  25575  tdeglem4  26228  plypf1  26380  tayl0  26536  taylthlem1  26547  xrlimcnp  27144  nosupno  27878  noinfno  27893  abrexexd  32866  ofpreima  33021  fisuppov1  33039  mptiffisupp  33049  mptctf  33072  gsummptres2  33382  psgnfzto1stlem  33429  rmfsupp2  33566  elrspunidl  33745  elrspunsn  33746  psrmonmul  33949  locfinreflem  34239  measdivcstALTV  34624  sitgf  34746  imageval  36428  poimirlem30  38329  poimir  38332  evlselv  43349  mhphf  43357  choicefi  45945  rn1st  46016  fourierdlem80  46928  sge0tsms  47122  scmsuppss  49179  rmfsupp  49181  scmfsupp  49183  fdivval  49347