Theorem funmpt 6578

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {copab 5166   ↦ cmpt 5185  Fun wfun 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-fun 6540

This theorem is used by:  funmpt2  6579  resfunexg  7221  mptexg  7227  mptexgf  7228  mptexw  7965  brtpos2  8250  tposfun  8260  mptfi  9341  fsuppssov1  9377  sniffsupp  9393  cantnfrescl  9678  cantnflem1  9691  r0weon  10092  axcc2lem  10515  mptct  10623  negfi  12267  mptnn0fsupp  14141  ccatalpha  14741  mreacs  17833  acsfn  17834  isofval  17933  lubfun  18525  glbfun  18538  acsficl2d  18727  gsum2dlem2  20186  gsum2d  20187  dprdfinv  20236  dprdfadd  20237  dmdprdsplitlem  20254  dpjidcl  20275  mptscmfsupp0  21203  pjpm  22015  frlmphllem  22087  uvcff  22098  uvcresum  22100  psrass1lem  22242  psrlidm  22270  psrridm  22271  psrass1  22272  psrass23l  22275  psrcom  22276  psrass23  22277  mplsubrg  22313  mplmon  22345  mplmonmul  22346  mplcoe1  22347  mplcoe5  22350  mplbas2  22352  evlslem2  22389  evlslem6  22391  evlsvvvallem2  22402  evlsvvval  22403  selvvvval  22452  psdmplcl  22484  psdmul  22488  psropprmul  22556  coe1mul2  22589  evls1fpws  22688  oftpos  22768  pmatcollpw2lem  23096  tgrest  23478  cmpfi  23727  1stcrestlem  23771  ptcnplem  23941  xkoinjcn  24007  symgtgp  24426  eltsms  24453  rrxmval  25727  tdeglem4  26379  plypf1  26532  tayl0  26690  taylthlem1  26701  xrlimcnp  27297  nosupno  28061  noinfno  28076  abrexexd  33148  ofpreima  33302  fisuppov1  33319  mptiffisupp  33329  mptctf  33351  gsummptres2  33657  psgnfzto1stlem  33704  rmfsupp2  33841  elrspunidl  34021  elrspunsn  34022  psrmonmul  34225  locfinreflem  34515  measdivcstALTV  34901  sitgf  35022  imageval  36767  poimirlem30  38644  poimir  38647  evlselv  43693  mhphf  43701  choicefi  46290  rn1st  46361  fourierdlem80  47272  sge0tsms  47466  tmachlem-agreefin  48034  scmsuppss  49559  rmfsupp  49561  scmfsupp  49563  fdivval  49727