Theorem funmpt 6515

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2110  {copab 5151   ↦ cmpt 5170  Fun wfun 6471

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-fun 6479

This theorem is referenced by:  funmpt2  6516  resfunexg  7144  mptexg  7150  mptexgf  7151  mptexw  7880  brtpos2  8157  tposfun  8167  mptfi  9230  fsuppssov1  9263  sniffsupp  9279  cantnfrescl  9561  cantnflem1  9574  r0weon  9895  axcc2lem  10319  mptct  10421  negfi  12063  mptnn0fsupp  13896  ccatalpha  14493  mreacs  17556  acsfn  17557  isofval  17656  lubfun  18248  glbfun  18261  acsficl2d  18450  gsum2dlem2  19876  gsum2d  19877  dprdfinv  19926  dprdfadd  19927  dmdprdsplitlem  19944  dpjidcl  19965  mptscmfsupp0  20853  pjpm  21638  frlmphllem  21710  uvcff  21721  uvcresum  21723  psrass1lem  21862  psrlidm  21892  psrridm  21893  psrass1  21894  psrass23l  21897  psrcom  21898  psrass23  21899  mplsubrg  21935  mplmon  21963  mplmonmul  21964  mplcoe1  21965  mplcoe5  21968  mplbas2  21970  evlslem2  22007  evlslem6  22009  psdmplcl  22070  psdmul  22074  psropprmul  22143  coe1mul2  22176  evls1fpws  22277  oftpos  22360  pmatcollpw2lem  22685  tgrest  23067  cmpfi  23316  1stcrestlem  23360  ptcnplem  23529  xkoinjcn  23595  symgtgp  24014  eltsms  24041  rrxmval  25325  tdeglem4  25985  plypf1  26137  tayl0  26289  taylthlem1  26301  xrlimcnp  26898  nosupno  27635  noinfno  27650  abrexexd  32479  ofpreima  32637  fisuppov1  32654  mptiffisupp  32664  mptctf  32689  gsummptres2  33023  psgnfzto1stlem  33059  rmfsupp2  33195  elrspunidl  33383  elrspunsn  33384  locfinreflem  33843  measdivcstALTV  34228  sitgf  34350  imageval  35943  poimirlem30  37669  poimir  37672  evlsvvvallem2  42574  evlsvvval  42575  selvvvval  42597  evlselv  42599  mhphf  42609  choicefi  45216  rn1st  45289  fourierdlem80  46203  sge0tsms  46397  scmsuppss  48381  rmfsupp  48383  scmfsupp  48385  fdivval  48550