Theorem funmpt 6039

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

Syntax hints:   ∧ wa 383   = wceq 1596   ∈ wcel 2103  {copab 4820   ↦ cmpt 4837  Fun wfun 5995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-fun 6003

This theorem is referenced by:  funmpt2  6040  resfunexg  6595  mptexg  6600  mptexgf  6601  brtpos2  7478  tposfun  7488  mptfi  8381  sniffsupp  8431  cantnfrescl  8686  cantnflem1  8699  r0weon  8948  axcc2lem  9371  mptct  9473  negfi  11084  mptnn0fsupp  12912  ccatalpha  13486  mreacs  16441  acsfn  16442  isofval  16539  lubfun  17102  glbfun  17115  acsficl2d  17298  pmtrsn  18060  gsum2dlem2  18491  gsum2d  18492  dprdfinv  18539  dprdfadd  18540  dmdprdsplitlem  18557  dpjidcl  18578  mptscmfsupp0  19051  00lsp  19104  psrass1lem  19500  psrlidm  19526  psrridm  19527  psrass1  19528  psrass23l  19531  psrcom  19532  psrass23  19533  mplsubrg  19563  mplmon  19586  mplmonmul  19587  mplcoe1  19588  mplcoe5  19591  mplbas2  19593  evlslem2  19635  evlslem6  19636  psropprmul  19731  coe1mul2  19762  pjpm  20175  frlmphllem  20242  frlmphl  20243  uvcff  20253  uvcresum  20255  oftpos  20381  pmatcollpw2lem  20705  tgrest  21086  cmpfi  21334  1stcrestlem  21378  ptcnplem  21547  xkoinjcn  21613  symgtgp  22027  eltsms  22058  rrxmval  23309  tdeglem4  23940  plypf1  24088  tayl0  24236  taylthlem1  24247  xrlimcnp  24815  abrexexd  29575  fmptcof2  29687  ofpreima  29695  funcnvmptOLD  29697  mptctf  29725  psgnfzto1stlem  30080  locfinreflem  30137  measdivcstOLD  30517  sxbrsigalem0  30563  sitgf  30639  nosupno  32076  imageval  32264  poimirlem30  33671  poimir  33674  choicefi  39808  fourierdlem80  40823  sge0tsms  41017  scmsuppss  42580  rmfsupp  42582  scmfsupp  42586  fdivval  42760