Theorem funmpt 6563

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

Syntax hints:   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {copab 5167   ↦ cmpt 5186  Fun wfun 6519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-fun 6527

This theorem is referenced by:  funmpt2  6564  resfunexg  7203  mptexg  7209  mptexgf  7210  mptexw  7938  brtpos2  8216  tposfun  8226  mptfi  9296  fsuppssov1  9332  sniffsupp  9348  cantnfrescl  9633  cantnflem1  9646  r0weon  9984  axcc2lem  10408  mptct  10510  negfi  12155  mptnn0fsupp  14024  ccatalpha  14621  mreacs  17704  acsfn  17705  isofval  17804  lubfun  18396  glbfun  18409  acsficl2d  18598  gsum2dlem2  20032  gsum2d  20033  dprdfinv  20082  dprdfadd  20083  dmdprdsplitlem  20100  dpjidcl  20121  mptscmfsupp0  21017  pjpm  21818  frlmphllem  21890  uvcff  21901  uvcresum  21903  psrass1lem  22043  psrlidm  22071  psrridm  22072  psrass1  22073  psrass23l  22076  psrcom  22077  psrass23  22078  mplsubrg  22114  mplmon  22146  mplmonmul  22147  mplcoe1  22148  mplcoe5  22151  mplbas2  22153  evlslem2  22190  evlslem6  22192  evlsvvvallem2  22203  evlsvvval  22204  selvvvval  22253  psdmplcl  22285  psdmul  22289  psropprmul  22357  coe1mul2  22390  evls1fpws  22490  oftpos  22570  pmatcollpw2lem  22895  tgrest  23277  cmpfi  23526  1stcrestlem  23570  ptcnplem  23739  xkoinjcn  23805  symgtgp  24224  eltsms  24251  rrxmval  25525  tdeglem4  26178  plypf1  26330  tayl0  26483  taylthlem1  26494  xrlimcnp  27091  nosupno  27825  noinfno  27840  abrexexd  32765  ofpreima  32922  fisuppov1  32940  mptiffisupp  32950  mptctf  32973  gsummptres2  33286  psgnfzto1stlem  33333  rmfsupp2  33470  elrspunidl  33652  elrspunsn  33653  psrmonmul  33857  locfinreflem  34147  measdivcstALTV  34532  sitgf  34654  imageval  36291  poimirlem30  38161  poimir  38164  evlselv  43183  mhphf  43191  choicefi  45775  rn1st  45846  fourierdlem80  46758  sge0tsms  46952  scmsuppss  49002  rmfsupp  49004  scmfsupp  49006  fdivval  49170