Theorem funmpt 6566

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5166   ↦ cmpt 5185  Fun wfun 6521

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-pr 5390

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-fun 6529

This theorem is used by:  funmpt2  6567  resfunexg  7209  mptexg  7215  mptexgf  7216  mptexw  7948  brtpos2  8227  tposfun  8237  mptfi  9318  fsuppssov1  9354  sniffsupp  9370  cantnfrescl  9655  cantnflem1  9668  r0weon  10063  axcc2lem  10486  mptct  10594  negfi  12236  mptnn0fsupp  14109  ccatalpha  14708  mreacs  17794  acsfn  17795  isofval  17894  lubfun  18486  glbfun  18499  acsficl2d  18688  gsum2dlem2  20147  gsum2d  20148  dprdfinv  20197  dprdfadd  20198  dmdprdsplitlem  20215  dpjidcl  20236  mptscmfsupp0  21164  pjpm  21976  frlmphllem  22048  uvcff  22059  uvcresum  22061  psrass1lem  22203  psrlidm  22231  psrridm  22232  psrass1  22233  psrass23l  22236  psrcom  22237  psrass23  22238  mplsubrg  22274  mplmon  22306  mplmonmul  22307  mplcoe1  22308  mplcoe5  22311  mplbas2  22313  evlslem2  22350  evlslem6  22352  evlsvvvallem2  22363  evlsvvval  22364  selvvvval  22413  psdmplcl  22445  psdmul  22449  psropprmul  22517  coe1mul2  22550  evls1fpws  22649  oftpos  22729  pmatcollpw2lem  23057  tgrest  23439  cmpfi  23688  1stcrestlem  23732  ptcnplem  23902  xkoinjcn  23968  symgtgp  24387  eltsms  24414  rrxmval  25688  tdeglem4  26340  plypf1  26493  tayl0  26653  taylthlem1  26664  xrlimcnp  27260  nosupno  27994  noinfno  28009  abrexexd  33039  ofpreima  33193  fisuppov1  33210  mptiffisupp  33220  mptctf  33242  gsummptres2  33548  psgnfzto1stlem  33595  rmfsupp2  33732  elrspunidl  33912  elrspunsn  33913  psrmonmul  34116  locfinreflem  34406  measdivcstALTV  34792  sitgf  34914  imageval  36614  poimirlem30  38488  poimir  38491  evlselv  43539  mhphf  43547  choicefi  46135  rn1st  46206  fourierdlem80  47118  sge0tsms  47312  tmachlem-agreefin  47880  scmsuppss  49405  rmfsupp  49407  scmfsupp  49409  fdivval  49573