Theorem funmpt 6598

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {copab 5170   ↦ cmpt 5189  Fun wfun 6552

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-fun 6560

This theorem is used by:  funmpt2  6599  resfunexg  7244  mptexg  7250  mptexgf  7251  mptexw  7989  brtpos2  8277  tposfun  8287  mptfi  9368  fsuppssov1  9403  sniffsupp  9419  cantnfrescl  9704  cantnflem1  9717  r0weon  10118  axcc2lem  10541  mptct  10649  negfi  12293  mptnn0fsupp  14167  ccatalpha  14767  mreacs  17861  acsfn  17862  isofval  17961  lubfun  18553  glbfun  18566  acsficl2d  18755  gsum2dlem2  20215  gsum2d  20216  dprdfinv  20265  dprdfadd  20266  dmdprdsplitlem  20283  dpjidcl  20304  mptscmfsupp0  21232  pjpm  22044  frlmphllem  22116  uvcff  22127  uvcresum  22129  psrass1lem  22271  psrlidm  22299  psrridm  22300  psrass1  22301  psrass23l  22304  psrcom  22305  psrass23  22306  mplsubrg  22342  mplmon  22374  mplmonmul  22375  mplcoe1  22376  mplcoe5  22379  mplbas2  22381  evlslem2  22418  evlslem6  22420  evlsvvvallem2  22431  evlsvvval  22432  selvvvval  22481  psdmplcl  22513  psdmul  22517  psropprmul  22585  coe1mul2  22618  evls1fpws  22717  oftpos  22797  pmatcollpw2lem  23125  tgrest  23507  cmpfi  23756  1stcrestlem  23800  ptcnplem  23970  xkoinjcn  24036  symgtgp  24455  eltsms  24482  rrxmval  25756  tdeglem4  26408  plypf1  26561  tayl0  26719  taylthlem1  26730  xrlimcnp  27326  nosupno  28090  noinfno  28105  abrexexd  33177  ofpreima  33331  fisuppov1  33347  mptiffisupp  33357  mptctf  33379  gsummptres2  33684  psgnfzto1stlem  33731  rmfsupp2  33868  elrspunidl  34048  elrspunsn  34049  psrmonmul  34252  locfinreflem  34542  measdivcstALTV  34928  sitgf  35049  imageval  36870  poimirlem30  38760  poimir  38763  evlselv  43810  mhphf  43818  choicefi  46419  rn1st  46490  fourierdlem80  47401  sge0tsms  47595  tmachlem-agreefin  48163  scmsuppss  49688  rmfsupp  49690  scmfsupp  49692  fdivval  49856