Theorem funmpt 6554

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5169   ↦ cmpt 5188  Fun wfun 6505

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6513

This theorem is referenced by:  funmpt2  6555  resfunexg  7189  mptexg  7195  mptexgf  7196  mptexw  7931  brtpos2  8211  tposfun  8221  mptfi  9302  fsuppssov1  9335  sniffsupp  9351  cantnfrescl  9629  cantnflem1  9642  r0weon  9965  axcc2lem  10389  mptct  10491  negfi  12132  mptnn0fsupp  13962  ccatalpha  14558  mreacs  17619  acsfn  17620  isofval  17719  lubfun  18311  glbfun  18324  acsficl2d  18511  gsum2dlem2  19901  gsum2d  19902  dprdfinv  19951  dprdfadd  19952  dmdprdsplitlem  19969  dpjidcl  19990  mptscmfsupp0  20833  pjpm  21617  frlmphllem  21689  uvcff  21700  uvcresum  21702  psrass1lem  21841  psrlidm  21871  psrridm  21872  psrass1  21873  psrass23l  21876  psrcom  21877  psrass23  21878  mplsubrg  21914  mplmon  21942  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  mplbas2  21949  evlslem2  21986  evlslem6  21988  psdmplcl  22049  psdmul  22053  psropprmul  22122  coe1mul2  22155  evls1fpws  22256  oftpos  22339  pmatcollpw2lem  22664  tgrest  23046  cmpfi  23295  1stcrestlem  23339  ptcnplem  23508  xkoinjcn  23574  symgtgp  23993  eltsms  24020  rrxmval  25305  tdeglem4  25965  plypf1  26117  tayl0  26269  taylthlem1  26281  xrlimcnp  26878  nosupno  27615  noinfno  27630  abrexexd  32438  ofpreima  32589  fisuppov1  32606  mptiffisupp  32616  mptctf  32641  gsummptres2  32993  psgnfzto1stlem  33057  rmfsupp2  33189  elrspunidl  33399  elrspunsn  33400  locfinreflem  33830  measdivcstALTV  34215  sitgf  34338  imageval  35918  poimirlem30  37644  poimir  37647  evlsvvvallem2  42550  evlsvvval  42551  selvvvval  42573  evlselv  42575  mhphf  42585  choicefi  45194  rn1st  45267  fourierdlem80  46184  sge0tsms  46378  scmsuppss  48359  rmfsupp  48361  scmfsupp  48363  fdivval  48528