Theorem funmpt 6575

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5171   ↦ cmpt 5190  Fun wfun 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-fun 6539

This theorem is used by:  funmpt2  6576  resfunexg  7217  mptexg  7223  mptexgf  7224  mptexw  7953  brtpos2  8233  tposfun  8243  mptfi  9321  fsuppssov1  9357  sniffsupp  9373  cantnfrescl  9658  cantnflem1  9671  r0weon  10018  axcc2lem  10441  mptct  10549  negfi  12191  mptnn0fsupp  14063  ccatalpha  14662  mreacs  17750  acsfn  17751  isofval  17850  lubfun  18442  glbfun  18455  acsficl2d  18644  gsum2dlem2  20102  gsum2d  20103  dprdfinv  20152  dprdfadd  20153  dmdprdsplitlem  20170  dpjidcl  20191  mptscmfsupp0  21115  pjpm  21925  frlmphllem  21997  uvcff  22008  uvcresum  22010  psrass1lem  22152  psrlidm  22180  psrridm  22181  psrass1  22182  psrass23l  22185  psrcom  22186  psrass23  22187  mplsubrg  22223  mplmon  22255  mplmonmul  22256  mplcoe1  22257  mplcoe5  22260  mplbas2  22262  evlslem2  22299  evlslem6  22301  evlsvvvallem2  22312  evlsvvval  22313  selvvvval  22362  psdmplcl  22394  psdmul  22398  psropprmul  22466  coe1mul2  22499  evls1fpws  22598  oftpos  22678  pmatcollpw2lem  23006  tgrest  23388  cmpfi  23637  1stcrestlem  23681  ptcnplem  23851  xkoinjcn  23917  symgtgp  24336  eltsms  24363  rrxmval  25637  tdeglem4  26290  plypf1  26442  tayl0  26598  taylthlem1  26609  xrlimcnp  27206  nosupno  27940  noinfno  27955  abrexexd  32985  ofpreima  33140  fisuppov1  33157  mptiffisupp  33167  mptctf  33189  gsummptres2  33495  psgnfzto1stlem  33542  rmfsupp2  33679  elrspunidl  33858  elrspunsn  33859  psrmonmul  34062  locfinreflem  34352  measdivcstALTV  34738  sitgf  34860  imageval  36509  poimirlem30  38401  poimir  38404  evlselv  43437  mhphf  43445  choicefi  46033  rn1st  46104  fourierdlem80  47016  sge0tsms  47210  tmachlem-agreefin  47778  scmsuppss  49303  rmfsupp  49305  scmfsupp  49307  fdivval  49471