Theorem funmpt 6525

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {copab 5155   ↦ cmpt 5174  Fun wfun 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-fun 6489

This theorem is referenced by:  funmpt2  6526  resfunexg  7155  mptexg  7161  mptexgf  7162  mptexw  7891  brtpos2  8168  tposfun  8178  mptfi  9241  fsuppssov1  9274  sniffsupp  9290  cantnfrescl  9572  cantnflem1  9585  r0weon  9909  axcc2lem  10333  mptct  10435  negfi  12077  mptnn0fsupp  13910  ccatalpha  14507  mreacs  17570  acsfn  17571  isofval  17670  lubfun  18262  glbfun  18275  acsficl2d  18464  gsum2dlem2  19889  gsum2d  19890  dprdfinv  19939  dprdfadd  19940  dmdprdsplitlem  19957  dpjidcl  19978  mptscmfsupp0  20866  pjpm  21651  frlmphllem  21723  uvcff  21734  uvcresum  21736  psrass1lem  21875  psrlidm  21905  psrridm  21906  psrass1  21907  psrass23l  21910  psrcom  21911  psrass23  21912  mplsubrg  21948  mplmon  21976  mplmonmul  21977  mplcoe1  21978  mplcoe5  21981  mplbas2  21983  evlslem2  22020  evlslem6  22022  psdmplcl  22083  psdmul  22087  psropprmul  22156  coe1mul2  22189  evls1fpws  22290  oftpos  22373  pmatcollpw2lem  22698  tgrest  23080  cmpfi  23329  1stcrestlem  23373  ptcnplem  23542  xkoinjcn  23608  symgtgp  24027  eltsms  24054  rrxmval  25338  tdeglem4  25998  plypf1  26150  tayl0  26302  taylthlem1  26314  xrlimcnp  26911  nosupno  27648  noinfno  27663  abrexexd  32496  ofpreima  32654  fisuppov1  32671  mptiffisupp  32681  mptctf  32706  gsummptres2  33040  psgnfzto1stlem  33076  rmfsupp2  33212  elrspunidl  33400  elrspunsn  33401  locfinreflem  33860  measdivcstALTV  34245  sitgf  34367  imageval  35979  poimirlem30  37696  poimir  37699  evlsvvvallem2  42661  evlsvvval  42662  selvvvval  42684  evlselv  42686  mhphf  42696  choicefi  45302  rn1st  45375  fourierdlem80  46289  sge0tsms  46483  scmsuppss  48476  rmfsupp  48478  scmfsupp  48480  fdivval  48645