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 (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 400   = wceq 1568   ∈ wcel 2141  {copab 5172   ↦ cmpt 5191  Fun wfun 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  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 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-fun 6538

This theorem is referenced by:  funmpt2  6575  resfunexg  7213  mptexg  7219  mptexgf  7220  mptexw  7949  brtpos2  8227  tposfun  8237  mptfi  9307  fsuppssov1  9343  sniffsupp  9359  cantnfrescl  9644  cantnflem1  9657  r0weon  9995  axcc2lem  10419  mptct  10521  negfi  12163  mptnn0fsupp  14033  ccatalpha  14631  mreacs  17713  acsfn  17714  isofval  17813  lubfun  18405  glbfun  18418  acsficl2d  18607  gsum2dlem2  20040  gsum2d  20041  dprdfinv  20090  dprdfadd  20091  dmdprdsplitlem  20108  dpjidcl  20129  mptscmfsupp0  21027  pjpm  21837  frlmphllem  21909  uvcff  21920  uvcresum  21922  psrass1lem  22062  psrlidm  22090  psrridm  22091  psrass1  22092  psrass23l  22095  psrcom  22096  psrass23  22097  mplsubrg  22133  mplmon  22165  mplmonmul  22166  mplcoe1  22167  mplcoe5  22170  mplbas2  22172  evlslem2  22209  evlslem6  22211  evlsvvvallem2  22222  evlsvvval  22223  selvvvval  22272  psdmplcl  22304  psdmul  22308  psropprmul  22376  coe1mul2  22409  evls1fpws  22508  oftpos  22588  pmatcollpw2lem  22913  tgrest  23295  cmpfi  23544  1stcrestlem  23588  ptcnplem  23757  xkoinjcn  23823  symgtgp  24242  eltsms  24269  rrxmval  25543  tdeglem4  26196  plypf1  26348  tayl0  26501  taylthlem1  26512  xrlimcnp  27109  nosupno  27843  noinfno  27858  abrexexd  32821  ofpreima  32976  fisuppov1  32994  mptiffisupp  33004  mptctf  33027  gsummptres2  33339  psgnfzto1stlem  33386  rmfsupp2  33523  elrspunidl  33702  elrspunsn  33703  psrmonmul  33906  locfinreflem  34196  measdivcstALTV  34581  sitgf  34703  imageval  36386  poimirlem30  38267  poimir  38270  evlselv  43291  mhphf  43299  choicefi  45887  rn1st  45958  fourierdlem80  46870  sge0tsms  47064  scmsuppss  49118  rmfsupp  49120  scmfsupp  49122  fdivval  49286