Theorem funmpt 6538

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5162   ↦ cmpt 5181  Fun wfun 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-fun 6502

This theorem is referenced by:  funmpt2  6539  resfunexg  7171  mptexg  7177  mptexgf  7178  mptexw  7907  brtpos2  8184  tposfun  8194  mptfi  9263  fsuppssov1  9299  sniffsupp  9315  cantnfrescl  9597  cantnflem1  9610  r0weon  9934  axcc2lem  10358  mptct  10460  negfi  12103  mptnn0fsupp  13932  ccatalpha  14529  mreacs  17593  acsfn  17594  isofval  17693  lubfun  18285  glbfun  18298  acsficl2d  18487  gsum2dlem2  19912  gsum2d  19913  dprdfinv  19962  dprdfadd  19963  dmdprdsplitlem  19980  dpjidcl  20001  mptscmfsupp0  20890  pjpm  21675  frlmphllem  21747  uvcff  21758  uvcresum  21760  psrass1lem  21900  psrlidm  21929  psrridm  21930  psrass1  21931  psrass23l  21934  psrcom  21935  psrass23  21936  mplsubrg  21972  mplmon  22002  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  mplbas2  22009  evlslem2  22046  evlslem6  22048  evlsvvvallem2  22059  evlsvvval  22060  psdmplcl  22117  psdmul  22121  psropprmul  22190  coe1mul2  22223  evls1fpws  22325  oftpos  22408  pmatcollpw2lem  22733  tgrest  23115  cmpfi  23364  1stcrestlem  23408  ptcnplem  23577  xkoinjcn  23643  symgtgp  24062  eltsms  24089  rrxmval  25373  tdeglem4  26033  plypf1  26185  tayl0  26337  taylthlem1  26349  xrlimcnp  26946  nosupno  27683  noinfno  27698  abrexexd  32595  ofpreima  32754  fisuppov1  32772  mptiffisupp  32782  mptctf  32805  gsummptres2  33146  psgnfzto1stlem  33193  rmfsupp2  33331  elrspunidl  33520  elrspunsn  33521  psrmonmul  33726  locfinreflem  34017  measdivcstALTV  34402  sitgf  34524  imageval  36141  poimirlem30  37890  poimir  37893  selvvvval  42932  evlselv  42934  mhphf  42944  choicefi  45547  rn1st  45620  fourierdlem80  46533  sge0tsms  46727  scmsuppss  48720  rmfsupp  48722  scmfsupp  48724  fdivval  48888