Theorem funmpt 6530

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

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {copab 5141   ↦ cmpt 5160  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6494

This theorem is referenced by:  funmpt2  6531  resfunexg  7166  mptexg  7172  mptexgf  7173  mptexw  7902  brtpos2  8179  tposfun  8189  mptfi  9258  fsuppssov1  9294  sniffsupp  9310  cantnfrescl  9595  cantnflem1  9608  r0weon  9932  axcc2lem  10356  mptct  10458  negfi  12103  mptnn0fsupp  13957  ccatalpha  14554  mreacs  17622  acsfn  17623  isofval  17722  lubfun  18314  glbfun  18327  acsficl2d  18516  gsum2dlem2  19944  gsum2d  19945  dprdfinv  19994  dprdfadd  19995  dmdprdsplitlem  20012  dpjidcl  20033  mptscmfsupp0  20924  pjpm  21690  frlmphllem  21762  uvcff  21773  uvcresum  21775  psrass1lem  21915  psrlidm  21943  psrridm  21944  psrass1  21945  psrass23l  21948  psrcom  21949  psrass23  21950  mplsubrg  21986  mplmon  22018  mplmonmul  22019  mplcoe1  22020  mplcoe5  22023  mplbas2  22025  evlslem2  22062  evlslem6  22064  evlsvvvallem2  22075  evlsvvval  22076  selvvvval  22125  psdmplcl  22157  psdmul  22161  psropprmul  22229  coe1mul2  22262  evls1fpws  22362  oftpos  22442  pmatcollpw2lem  22767  tgrest  23149  cmpfi  23398  1stcrestlem  23442  ptcnplem  23611  xkoinjcn  23677  symgtgp  24096  eltsms  24123  rrxmval  25397  tdeglem4  26050  plypf1  26202  tayl0  26352  taylthlem1  26363  xrlimcnp  26957  nosupno  27692  noinfno  27707  abrexexd  32604  ofpreima  32764  fisuppov1  32782  mptiffisupp  32792  mptctf  32815  gsummptres2  33141  psgnfzto1stlem  33188  rmfsupp2  33326  elrspunidl  33518  elrspunsn  33519  psrmonmul  33741  locfinreflem  34031  measdivcstALTV  34416  sitgf  34538  imageval  36157  poimirlem30  38018  poimir  38021  evlselv  43040  mhphf  43048  choicefi  45647  rn1st  45718  fourierdlem80  46630  sge0tsms  46824  scmsuppss  48863  rmfsupp  48865  scmfsupp  48867  fdivval  49031