Theorem funmpt 6557

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5172   ↦ cmpt 5191  Fun wfun 6508

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  funmpt2  6558  resfunexg  7192  mptexg  7198  mptexgf  7199  mptexw  7934  brtpos2  8214  tposfun  8224  mptfi  9309  fsuppssov1  9342  sniffsupp  9358  cantnfrescl  9636  cantnflem1  9649  r0weon  9972  axcc2lem  10396  mptct  10498  negfi  12139  mptnn0fsupp  13969  ccatalpha  14565  mreacs  17626  acsfn  17627  isofval  17726  lubfun  18318  glbfun  18331  acsficl2d  18518  gsum2dlem2  19908  gsum2d  19909  dprdfinv  19958  dprdfadd  19959  dmdprdsplitlem  19976  dpjidcl  19997  mptscmfsupp0  20840  pjpm  21624  frlmphllem  21696  uvcff  21707  uvcresum  21709  psrass1lem  21848  psrlidm  21878  psrridm  21879  psrass1  21880  psrass23l  21883  psrcom  21884  psrass23  21885  mplsubrg  21921  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplcoe5  21954  mplbas2  21956  evlslem2  21993  evlslem6  21995  psdmplcl  22056  psdmul  22060  psropprmul  22129  coe1mul2  22162  evls1fpws  22263  oftpos  22346  pmatcollpw2lem  22671  tgrest  23053  cmpfi  23302  1stcrestlem  23346  ptcnplem  23515  xkoinjcn  23581  symgtgp  24000  eltsms  24027  rrxmval  25312  tdeglem4  25972  plypf1  26124  tayl0  26276  taylthlem1  26288  xrlimcnp  26885  nosupno  27622  noinfno  27637  abrexexd  32445  ofpreima  32596  fisuppov1  32613  mptiffisupp  32623  mptctf  32648  gsummptres2  33000  psgnfzto1stlem  33064  rmfsupp2  33196  elrspunidl  33406  elrspunsn  33407  locfinreflem  33837  measdivcstALTV  34222  sitgf  34345  imageval  35925  poimirlem30  37651  poimir  37654  evlsvvvallem2  42557  evlsvvval  42558  selvvvval  42580  evlselv  42582  mhphf  42592  choicefi  45201  rn1st  45274  fourierdlem80  46191  sge0tsms  46385  scmsuppss  48363  rmfsupp  48365  scmfsupp  48367  fdivval  48532