Theorem funmpt 6616

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

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {copab 5228   ↦ cmpt 5249  Fun wfun 6567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-fun 6575

This theorem is referenced by:  funmpt2  6617  resfunexg  7252  mptexg  7258  mptexgf  7259  mptexw  7993  brtpos2  8273  tposfun  8283  mptfi  9421  fsuppssov1  9453  sniffsupp  9469  cantnfrescl  9745  cantnflem1  9758  r0weon  10081  axcc2lem  10505  mptct  10607  negfi  12244  mptnn0fsupp  14048  ccatalpha  14641  mreacs  17716  acsfn  17717  isofval  17818  lubfun  18422  glbfun  18435  acsficl2d  18622  gsum2dlem2  20013  gsum2d  20014  dprdfinv  20063  dprdfadd  20064  dmdprdsplitlem  20081  dpjidcl  20102  mptscmfsupp0  20947  pjpm  21751  frlmphllem  21823  uvcff  21834  uvcresum  21836  psrass1lem  21975  psrlidm  22005  psrridm  22006  psrass1  22007  psrass23l  22010  psrcom  22011  psrass23  22012  mplsubrg  22048  mplmon  22076  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  mplbas2  22083  evlslem2  22126  evlslem6  22128  psdmplcl  22189  psdmul  22193  psropprmul  22260  coe1mul2  22293  evls1fpws  22394  oftpos  22479  pmatcollpw2lem  22804  tgrest  23188  cmpfi  23437  1stcrestlem  23481  ptcnplem  23650  xkoinjcn  23716  symgtgp  24135  eltsms  24162  rrxmval  25458  tdeglem4  26119  plypf1  26271  tayl0  26421  taylthlem1  26433  xrlimcnp  27029  nosupno  27766  noinfno  27781  abrexexd  32537  ofpreima  32683  mptiffisupp  32705  mptctf  32731  gsummptres2  33036  psgnfzto1stlem  33093  rmfsupp2  33218  elrspunidl  33421  elrspunsn  33422  locfinreflem  33786  measdivcstALTV  34189  sitgf  34312  imageval  35894  poimirlem30  37610  poimir  37613  evlsvvvallem2  42517  evlsvvval  42518  selvvvval  42540  evlselv  42542  mhphf  42552  choicefi  45107  rn1st  45183  fourierdlem80  46107  sge0tsms  46301  scmsuppss  48097  rmfsupp  48099  scmfsupp  48103  fdivval  48273