Theorem funmpt 6528

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5148   ↦ cmpt 5167  Fun wfun 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-fun 6492

This theorem is referenced by:  funmpt2  6529  resfunexg  7161  mptexg  7167  mptexgf  7168  mptexw  7897  brtpos2  8173  tposfun  8183  mptfi  9252  fsuppssov1  9288  sniffsupp  9304  cantnfrescl  9586  cantnflem1  9599  r0weon  9923  axcc2lem  10347  mptct  10449  negfi  12094  mptnn0fsupp  13948  ccatalpha  14545  mreacs  17613  acsfn  17614  isofval  17713  lubfun  18305  glbfun  18318  acsficl2d  18507  gsum2dlem2  19935  gsum2d  19936  dprdfinv  19985  dprdfadd  19986  dmdprdsplitlem  20003  dpjidcl  20024  mptscmfsupp0  20911  pjpm  21696  frlmphllem  21768  uvcff  21779  uvcresum  21781  psrass1lem  21920  psrlidm  21949  psrridm  21950  psrass1  21951  psrass23l  21954  psrcom  21955  psrass23  21956  mplsubrg  21992  mplmon  22022  mplmonmul  22023  mplcoe1  22024  mplcoe5  22027  mplbas2  22029  evlslem2  22066  evlslem6  22068  evlsvvvallem2  22079  evlsvvval  22080  psdmplcl  22137  psdmul  22141  psropprmul  22210  coe1mul2  22243  evls1fpws  22343  oftpos  22426  pmatcollpw2lem  22751  tgrest  23133  cmpfi  23382  1stcrestlem  23426  ptcnplem  23595  xkoinjcn  23661  symgtgp  24080  eltsms  24107  rrxmval  25381  tdeglem4  26037  plypf1  26189  tayl0  26340  taylthlem1  26352  xrlimcnp  26949  nosupno  27686  noinfno  27701  abrexexd  32599  ofpreima  32758  fisuppov1  32776  mptiffisupp  32786  mptctf  32809  gsummptres2  33134  psgnfzto1stlem  33181  rmfsupp2  33319  elrspunidl  33508  elrspunsn  33509  psrmonmul  33714  locfinreflem  34005  measdivcstALTV  34390  sitgf  34512  imageval  36131  poimirlem30  37982  poimir  37985  selvvvval  43029  evlselv  43031  mhphf  43041  choicefi  45644  rn1st  45717  fourierdlem80  46629  sge0tsms  46823  scmsuppss  48844  rmfsupp  48846  scmfsupp  48848  fdivval  49012