Theorem funmpt 6548

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

Syntax hints:   ∧ wa 398   = wceq 1554   ∈ wcel 2136  {copab 5156   ↦ cmpt 5175  Fun wfun 6504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-fun 6512

This theorem is referenced by:  funmpt2  6549  resfunexg  7188  mptexg  7194  mptexgf  7195  mptexw  7923  brtpos2  8200  tposfun  8210  mptfi  9284  fsuppssov1  9320  sniffsupp  9336  cantnfrescl  9621  cantnflem1  9634  r0weon  9958  axcc2lem  10383  mptct  10485  negfi  12131  mptnn0fsupp  14000  ccatalpha  14597  mreacs  17666  acsfn  17667  isofval  17766  lubfun  18358  glbfun  18371  acsficl2d  18560  gsum2dlem2  19987  gsum2d  19988  dprdfinv  20037  dprdfadd  20038  dmdprdsplitlem  20055  dpjidcl  20076  mptscmfsupp0  20967  pjpm  21733  frlmphllem  21805  uvcff  21816  uvcresum  21818  psrass1lem  21958  psrlidm  21986  psrridm  21987  psrass1  21988  psrass23l  21991  psrcom  21992  psrass23  21993  mplsubrg  22029  mplmon  22061  mplmonmul  22062  mplcoe1  22063  mplcoe5  22066  mplbas2  22068  evlslem2  22105  evlslem6  22107  evlsvvvallem2  22118  evlsvvval  22119  selvvvval  22168  psdmplcl  22200  psdmul  22204  psropprmul  22272  coe1mul2  22305  evls1fpws  22405  oftpos  22485  pmatcollpw2lem  22810  tgrest  23192  cmpfi  23441  1stcrestlem  23485  ptcnplem  23654  xkoinjcn  23720  symgtgp  24139  eltsms  24166  rrxmval  25440  tdeglem4  26093  plypf1  26245  tayl0  26395  taylthlem1  26406  xrlimcnp  27003  nosupno  27737  noinfno  27752  abrexexd  32650  ofpreima  32810  fisuppov1  32828  mptiffisupp  32838  mptctf  32861  gsummptres2  33187  psgnfzto1stlem  33234  rmfsupp2  33372  elrspunidl  33568  elrspunsn  33569  psrmonmul  33801  locfinreflem  34091  measdivcstALTV  34476  sitgf  34598  imageval  36226  poimirlem30  38097  poimir  38100  evlselv  43119  mhphf  43127  choicefi  45725  rn1st  45796  fourierdlem80  46708  sge0tsms  46902  scmsuppss  48941  rmfsupp  48943  scmfsupp  48945  fdivval  49109