Theorem funmpt 6531

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5161   ↦ cmpt 5180  Fun wfun 6487

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6495

This theorem is referenced by:  funmpt2  6532  resfunexg  7163  mptexg  7169  mptexgf  7170  mptexw  7899  brtpos2  8176  tposfun  8186  mptfi  9255  fsuppssov1  9291  sniffsupp  9307  cantnfrescl  9589  cantnflem1  9602  r0weon  9926  axcc2lem  10350  mptct  10452  negfi  12095  mptnn0fsupp  13924  ccatalpha  14521  mreacs  17585  acsfn  17586  isofval  17685  lubfun  18277  glbfun  18290  acsficl2d  18479  gsum2dlem2  19904  gsum2d  19905  dprdfinv  19954  dprdfadd  19955  dmdprdsplitlem  19972  dpjidcl  19993  mptscmfsupp0  20882  pjpm  21667  frlmphllem  21739  uvcff  21750  uvcresum  21752  psrass1lem  21892  psrlidm  21921  psrridm  21922  psrass1  21923  psrass23l  21926  psrcom  21927  psrass23  21928  mplsubrg  21964  mplmon  21994  mplmonmul  21995  mplcoe1  21996  mplcoe5  21999  mplbas2  22001  evlslem2  22038  evlslem6  22040  evlsvvvallem2  22051  evlsvvval  22052  psdmplcl  22109  psdmul  22113  psropprmul  22182  coe1mul2  22215  evls1fpws  22317  oftpos  22400  pmatcollpw2lem  22725  tgrest  23107  cmpfi  23356  1stcrestlem  23400  ptcnplem  23569  xkoinjcn  23635  symgtgp  24054  eltsms  24081  rrxmval  25365  tdeglem4  26025  plypf1  26177  tayl0  26329  taylthlem1  26341  xrlimcnp  26938  nosupno  27675  noinfno  27690  abrexexd  32566  ofpreima  32725  fisuppov1  32743  mptiffisupp  32753  mptctf  32776  gsummptres2  33117  psgnfzto1stlem  33163  rmfsupp2  33301  elrspunidl  33490  elrspunsn  33491  locfinreflem  33978  measdivcstALTV  34363  sitgf  34485  imageval  36103  poimirlem30  37822  poimir  37825  selvvvval  42864  evlselv  42866  mhphf  42876  choicefi  45480  rn1st  45553  fourierdlem80  46466  sge0tsms  46660  scmsuppss  48653  rmfsupp  48655  scmfsupp  48657  fdivval  48821