Theorem funmpt 6524

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5157   ↦ cmpt 5176  Fun wfun 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-fun 6488

This theorem is referenced by:  funmpt2  6525  resfunexg  7155  mptexg  7161  mptexgf  7162  mptexw  7895  brtpos2  8172  tposfun  8182  mptfi  9260  fsuppssov1  9293  sniffsupp  9309  cantnfrescl  9591  cantnflem1  9604  r0weon  9925  axcc2lem  10349  mptct  10451  negfi  12092  mptnn0fsupp  13922  ccatalpha  14518  mreacs  17582  acsfn  17583  isofval  17682  lubfun  18274  glbfun  18287  acsficl2d  18476  gsum2dlem2  19868  gsum2d  19869  dprdfinv  19918  dprdfadd  19919  dmdprdsplitlem  19936  dpjidcl  19957  mptscmfsupp0  20848  pjpm  21633  frlmphllem  21705  uvcff  21716  uvcresum  21718  psrass1lem  21857  psrlidm  21887  psrridm  21888  psrass1  21889  psrass23l  21892  psrcom  21893  psrass23  21894  mplsubrg  21930  mplmon  21958  mplmonmul  21959  mplcoe1  21960  mplcoe5  21963  mplbas2  21965  evlslem2  22002  evlslem6  22004  psdmplcl  22065  psdmul  22069  psropprmul  22138  coe1mul2  22171  evls1fpws  22272  oftpos  22355  pmatcollpw2lem  22680  tgrest  23062  cmpfi  23311  1stcrestlem  23355  ptcnplem  23524  xkoinjcn  23590  symgtgp  24009  eltsms  24036  rrxmval  25321  tdeglem4  25981  plypf1  26133  tayl0  26285  taylthlem1  26297  xrlimcnp  26894  nosupno  27631  noinfno  27646  abrexexd  32471  ofpreima  32622  fisuppov1  32639  mptiffisupp  32649  mptctf  32674  gsummptres2  33019  psgnfzto1stlem  33055  rmfsupp2  33188  elrspunidl  33375  elrspunsn  33376  locfinreflem  33806  measdivcstALTV  34191  sitgf  34314  imageval  35903  poimirlem30  37629  poimir  37632  evlsvvvallem2  42535  evlsvvval  42536  selvvvval  42558  evlselv  42560  mhphf  42570  choicefi  45178  rn1st  45251  fourierdlem80  46168  sge0tsms  46362  scmsuppss  48343  rmfsupp  48345  scmfsupp  48347  fdivval  48512