Theorem funmpt 6574

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5181   ↦ cmpt 5201  Fun wfun 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-fun 6533

This theorem is referenced by:  funmpt2  6575  resfunexg  7207  mptexg  7213  mptexgf  7214  mptexw  7951  brtpos2  8231  tposfun  8241  mptfi  9363  fsuppssov1  9396  sniffsupp  9412  cantnfrescl  9690  cantnflem1  9703  r0weon  10026  axcc2lem  10450  mptct  10552  negfi  12191  mptnn0fsupp  14015  ccatalpha  14611  mreacs  17670  acsfn  17671  isofval  17770  lubfun  18362  glbfun  18375  acsficl2d  18562  gsum2dlem2  19952  gsum2d  19953  dprdfinv  20002  dprdfadd  20003  dmdprdsplitlem  20020  dpjidcl  20041  mptscmfsupp0  20884  pjpm  21668  frlmphllem  21740  uvcff  21751  uvcresum  21753  psrass1lem  21892  psrlidm  21922  psrridm  21923  psrass1  21924  psrass23l  21927  psrcom  21928  psrass23  21929  mplsubrg  21965  mplmon  21993  mplmonmul  21994  mplcoe1  21995  mplcoe5  21998  mplbas2  22000  evlslem2  22037  evlslem6  22039  psdmplcl  22100  psdmul  22104  psropprmul  22173  coe1mul2  22206  evls1fpws  22307  oftpos  22390  pmatcollpw2lem  22715  tgrest  23097  cmpfi  23346  1stcrestlem  23390  ptcnplem  23559  xkoinjcn  23625  symgtgp  24044  eltsms  24071  rrxmval  25357  tdeglem4  26017  plypf1  26169  tayl0  26321  taylthlem1  26333  xrlimcnp  26930  nosupno  27667  noinfno  27682  abrexexd  32490  ofpreima  32643  fisuppov1  32660  mptiffisupp  32670  mptctf  32695  gsummptres2  33047  psgnfzto1stlem  33111  rmfsupp2  33233  elrspunidl  33443  elrspunsn  33444  locfinreflem  33871  measdivcstALTV  34256  sitgf  34379  imageval  35948  poimirlem30  37674  poimir  37677  evlsvvvallem2  42585  evlsvvval  42586  selvvvval  42608  evlselv  42610  mhphf  42620  choicefi  45224  rn1st  45297  fourierdlem80  46215  sge0tsms  46409  scmsuppss  48346  rmfsupp  48348  scmfsupp  48350  fdivval  48519