Theorem funmpt 6527

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5157   ↦ cmpt 5176  Fun wfun 6483

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-fun 6491

This theorem is referenced by:  funmpt2  6528  resfunexg  7158  mptexg  7164  mptexgf  7165  mptexw  7894  brtpos2  8171  tposfun  8181  mptfi  9245  fsuppssov1  9278  sniffsupp  9294  cantnfrescl  9576  cantnflem1  9589  r0weon  9913  axcc2lem  10337  mptct  10439  negfi  12081  mptnn0fsupp  13914  ccatalpha  14511  mreacs  17574  acsfn  17575  isofval  17674  lubfun  18266  glbfun  18279  acsficl2d  18468  gsum2dlem2  19893  gsum2d  19894  dprdfinv  19943  dprdfadd  19944  dmdprdsplitlem  19961  dpjidcl  19982  mptscmfsupp0  20870  pjpm  21655  frlmphllem  21727  uvcff  21738  uvcresum  21740  psrass1lem  21879  psrlidm  21909  psrridm  21910  psrass1  21911  psrass23l  21914  psrcom  21915  psrass23  21916  mplsubrg  21952  mplmon  21980  mplmonmul  21981  mplcoe1  21982  mplcoe5  21985  mplbas2  21987  evlslem2  22024  evlslem6  22026  psdmplcl  22087  psdmul  22091  psropprmul  22160  coe1mul2  22193  evls1fpws  22294  oftpos  22377  pmatcollpw2lem  22702  tgrest  23084  cmpfi  23333  1stcrestlem  23377  ptcnplem  23546  xkoinjcn  23612  symgtgp  24031  eltsms  24058  rrxmval  25342  tdeglem4  26002  plypf1  26154  tayl0  26306  taylthlem1  26318  xrlimcnp  26915  nosupno  27652  noinfno  27667  abrexexd  32500  ofpreima  32658  fisuppov1  32675  mptiffisupp  32685  mptctf  32710  gsummptres2  33044  psgnfzto1stlem  33080  rmfsupp2  33216  elrspunidl  33404  elrspunsn  33405  locfinreflem  33864  measdivcstALTV  34249  sitgf  34371  imageval  35983  poimirlem30  37700  poimir  37703  evlsvvvallem2  42670  evlsvvval  42671  selvvvval  42693  evlselv  42695  mhphf  42705  choicefi  45311  rn1st  45384  fourierdlem80  46298  sge0tsms  46492  scmsuppss  48485  rmfsupp  48487  scmfsupp  48489  fdivval  48654