Theorem funmpt 6393

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {copab 5128   ↦ cmpt 5146  Fun wfun 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-fun 6357

This theorem is referenced by:  funmpt2  6394  resfunexg  6978  mptexg  6984  mptexgf  6985  mptexw  7654  brtpos2  7898  tposfun  7908  mptfi  8823  sniffsupp  8873  cantnfrescl  9139  cantnflem1  9152  r0weon  9438  axcc2lem  9858  mptct  9960  negfi  11589  mptnn0fsupp  13366  ccatalpha  13947  mreacs  16929  acsfn  16930  isofval  17027  lubfun  17590  glbfun  17603  acsficl2d  17786  gsum2dlem2  19091  gsum2d  19092  dprdfinv  19141  dprdfadd  19142  dmdprdsplitlem  19159  dpjidcl  19180  mptscmfsupp0  19699  psrass1lem  20157  psrlidm  20183  psrridm  20184  psrass1  20185  psrass23l  20188  psrcom  20189  psrass23  20190  mplsubrg  20220  mplmon  20244  mplmonmul  20245  mplcoe1  20246  mplcoe5  20249  mplbas2  20251  evlslem2  20292  evlslem6  20294  psropprmul  20406  coe1mul2  20437  pjpm  20852  frlmphllem  20924  frlmphl  20925  uvcff  20935  uvcresum  20937  oftpos  21061  pmatcollpw2lem  21385  tgrest  21767  cmpfi  22016  1stcrestlem  22060  ptcnplem  22229  xkoinjcn  22295  symgtgp  22714  eltsms  22741  rrxmval  24008  tdeglem4  24654  plypf1  24802  tayl0  24950  taylthlem1  24961  xrlimcnp  25546  abrexexd  30269  ofpreima  30410  mptctf  30453  psgnfzto1stlem  30742  rmfsupp2  30866  locfinreflem  31104  measdivcstALTV  31484  sxbrsigalem0  31529  sitgf  31605  nosupno  33203  imageval  33391  poimirlem30  34937  poimir  34940  choicefi  41512  fourierdlem80  42520  sge0tsms  42711  scmsuppss  44469  rmfsupp  44471  scmfsupp  44475  fdivval  44648