Theorem funmpt 6456

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {copab 5132   ↦ cmpt 5153  Fun wfun 6412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-fun 6420

This theorem is referenced by:  funmpt2  6457  resfunexg  7073  mptexg  7079  mptexgf  7080  mptexw  7769  brtpos2  8019  tposfun  8029  mptfi  9048  sniffsupp  9089  cantnfrescl  9364  cantnflem1  9377  r0weon  9699  axcc2lem  10123  mptct  10225  negfi  11854  mptnn0fsupp  13645  ccatalpha  14226  mreacs  17284  acsfn  17285  isofval  17386  lubfun  17985  glbfun  17998  acsficl2d  18185  gsum2dlem2  19487  gsum2d  19488  dprdfinv  19537  dprdfadd  19538  dmdprdsplitlem  19555  dpjidcl  19576  mptscmfsupp0  20103  pjpm  20825  frlmphllem  20897  frlmphl  20898  uvcff  20908  uvcresum  20910  psrass1lemOLD  21053  psrass1lem  21056  psrlidm  21082  psrridm  21083  psrass1  21084  psrass23l  21087  psrcom  21088  psrass23  21089  mplsubrg  21121  mplmon  21146  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  mplbas2  21153  evlslem2  21199  evlslem6  21201  psropprmul  21319  coe1mul2  21350  oftpos  21509  pmatcollpw2lem  21834  tgrest  22218  cmpfi  22467  1stcrestlem  22511  ptcnplem  22680  xkoinjcn  22746  symgtgp  23165  eltsms  23192  rrxmval  24474  tdeglem4  25129  tdeglem4OLD  25130  plypf1  25278  tayl0  25426  taylthlem1  25437  xrlimcnp  26023  abrexexd  30755  ofpreima  30904  mptctf  30954  gsummptres2  31215  psgnfzto1stlem  31269  rmfsupp2  31394  elrspunidl  31508  locfinreflem  31692  measdivcstALTV  32093  sxbrsigalem0  32138  sitgf  32214  nosupno  33833  noinfno  33848  imageval  34159  poimirlem30  35734  poimir  35737  evlsbagval  40198  mhphf  40208  choicefi  42629  fourierdlem80  43617  sge0tsms  43808  scmsuppss  45596  rmfsupp  45598  scmfsupp  45602  fdivval  45773