Theorem funmpt 6387

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

Syntax hints:   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {copab 5120   ↦ cmpt 5138  Fun wfun 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-fun 6351

This theorem is referenced by:  funmpt2  6388  resfunexg  6972  mptexg  6978  mptexgf  6979  mptexw  7648  brtpos2  7892  tposfun  7902  mptfi  8817  sniffsupp  8867  cantnfrescl  9133  cantnflem1  9146  r0weon  9432  axcc2lem  9852  mptct  9954  negfi  11583  mptnn0fsupp  13359  ccatalpha  13941  mreacs  16923  acsfn  16924  isofval  17021  lubfun  17584  glbfun  17597  acsficl2d  17780  gsum2dlem2  19085  gsum2d  19086  dprdfinv  19135  dprdfadd  19136  dmdprdsplitlem  19153  dpjidcl  19174  mptscmfsupp0  19693  psrass1lem  20151  psrlidm  20177  psrridm  20178  psrass1  20179  psrass23l  20182  psrcom  20183  psrass23  20184  mplsubrg  20214  mplmon  20238  mplmonmul  20239  mplcoe1  20240  mplcoe5  20243  mplbas2  20245  evlslem2  20286  evlslem6  20288  psropprmul  20400  coe1mul2  20431  pjpm  20846  frlmphllem  20918  frlmphl  20919  uvcff  20929  uvcresum  20931  oftpos  21055  pmatcollpw2lem  21379  tgrest  21761  cmpfi  22010  1stcrestlem  22054  ptcnplem  22223  xkoinjcn  22289  symgtgp  22708  eltsms  22735  rrxmval  24002  tdeglem4  24648  plypf1  24796  tayl0  24944  taylthlem1  24955  xrlimcnp  25540  abrexexd  30263  ofpreima  30404  mptctf  30447  psgnfzto1stlem  30737  rmfsupp2  30861  locfinreflem  31099  measdivcstALTV  31479  sxbrsigalem0  31524  sitgf  31600  nosupno  33198  imageval  33386  poimirlem30  34916  poimir  34919  choicefi  41456  fourierdlem80  42465  sge0tsms  42656  scmsuppss  44414  rmfsupp  44416  scmfsupp  44420  fdivval  44593