Theorem funmpt 6472

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {copab 5136   ↦ cmpt 5157  Fun wfun 6427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-fun 6435

This theorem is referenced by:  funmpt2  6473  resfunexg  7091  mptexg  7097  mptexgf  7098  mptexw  7795  brtpos2  8048  tposfun  8058  mptfi  9118  sniffsupp  9159  cantnfrescl  9434  cantnflem1  9447  r0weon  9768  axcc2lem  10192  mptct  10294  negfi  11924  mptnn0fsupp  13717  ccatalpha  14298  mreacs  17367  acsfn  17368  isofval  17469  lubfun  18070  glbfun  18083  acsficl2d  18270  gsum2dlem2  19572  gsum2d  19573  dprdfinv  19622  dprdfadd  19623  dmdprdsplitlem  19640  dpjidcl  19661  mptscmfsupp0  20188  pjpm  20915  frlmphllem  20987  frlmphl  20988  uvcff  20998  uvcresum  21000  psrass1lemOLD  21143  psrass1lem  21146  psrlidm  21172  psrridm  21173  psrass1  21174  psrass23l  21177  psrcom  21178  psrass23  21179  mplsubrg  21211  mplmon  21236  mplmonmul  21237  mplcoe1  21238  mplcoe5  21241  mplbas2  21243  evlslem2  21289  evlslem6  21291  psropprmul  21409  coe1mul2  21440  oftpos  21601  pmatcollpw2lem  21926  tgrest  22310  cmpfi  22559  1stcrestlem  22603  ptcnplem  22772  xkoinjcn  22838  symgtgp  23257  eltsms  23284  rrxmval  24569  tdeglem4  25224  tdeglem4OLD  25225  plypf1  25373  tayl0  25521  taylthlem1  25532  xrlimcnp  26118  abrexexd  30854  ofpreima  31002  mptctf  31052  gsummptres2  31313  psgnfzto1stlem  31367  rmfsupp2  31492  elrspunidl  31606  locfinreflem  31790  measdivcstALTV  32193  sxbrsigalem0  32238  sitgf  32314  nosupno  33906  noinfno  33921  imageval  34232  poimirlem30  35807  poimir  35810  evlsbagval  40275  mhphf  40285  prjcrv0  40470  choicefi  42740  fourierdlem80  43727  sge0tsms  43918  scmsuppss  45708  rmfsupp  45710  scmfsupp  45714  fdivval  45885