Theorem funmpt 6537

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5148   ↦ cmpt 5167  Fun wfun 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6501

This theorem is referenced by:  funmpt2  6538  resfunexg  7170  mptexg  7176  mptexgf  7177  mptexw  7906  brtpos2  8182  tposfun  8192  mptfi  9261  fsuppssov1  9297  sniffsupp  9313  cantnfrescl  9597  cantnflem1  9610  r0weon  9934  axcc2lem  10358  mptct  10460  negfi  12105  mptnn0fsupp  13959  ccatalpha  14556  mreacs  17624  acsfn  17625  isofval  17724  lubfun  18316  glbfun  18329  acsficl2d  18518  gsum2dlem2  19946  gsum2d  19947  dprdfinv  19996  dprdfadd  19997  dmdprdsplitlem  20014  dpjidcl  20035  mptscmfsupp0  20922  pjpm  21688  frlmphllem  21760  uvcff  21771  uvcresum  21773  psrass1lem  21912  psrlidm  21940  psrridm  21941  psrass1  21942  psrass23l  21945  psrcom  21946  psrass23  21947  mplsubrg  21983  mplmon  22013  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  mplbas2  22020  evlslem2  22057  evlslem6  22059  evlsvvvallem2  22070  evlsvvval  22071  psdmplcl  22128  psdmul  22132  psropprmul  22201  coe1mul2  22234  evls1fpws  22334  oftpos  22417  pmatcollpw2lem  22742  tgrest  23124  cmpfi  23373  1stcrestlem  23417  ptcnplem  23586  xkoinjcn  23652  symgtgp  24071  eltsms  24098  rrxmval  25372  tdeglem4  26025  plypf1  26177  tayl0  26327  taylthlem1  26338  xrlimcnp  26932  nosupno  27667  noinfno  27682  abrexexd  32579  ofpreima  32738  fisuppov1  32756  mptiffisupp  32766  mptctf  32789  gsummptres2  33114  psgnfzto1stlem  33161  rmfsupp2  33299  elrspunidl  33488  elrspunsn  33489  psrmonmul  33694  locfinreflem  33984  measdivcstALTV  34369  sitgf  34491  imageval  36110  poimirlem30  37971  poimir  37974  selvvvval  43018  evlselv  43020  mhphf  43030  choicefi  45629  rn1st  45702  fourierdlem80  46614  sge0tsms  46808  scmsuppss  48841  rmfsupp  48843  scmfsupp  48845  fdivval  49009