Theorem funres 6558

Description: A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)

Assertion

Ref	Expression
funres	⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

Proof of Theorem funres

Step	Hyp	Ref	Expression
1		resss 5983	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6535	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

Syntax hints:   → wi 4   ⊆ wss 3902   ↾ cres 5645  Fun wfun 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3909  df-ss 3919  df-br 5098  df-opab 5160  df-rel 5650  df-cnv 5651  df-co 5652  df-res 5655  df-fun 6518

This theorem is referenced by:  funresd  6559  fores  6783  resfunexg  7194  funfvima  7209  funiunfv  7227  fprlem1  8275  smores  8317  smores2  8319  frfnom  8400  sbthlem7  9059  fsuppres  9333  ordtypelem4  9463  wdomima2g  9528  imadomg  10485  hashres  14445  hashimarn  14447  setsfun  17198  setsfun0  17199  lubfun  18373  glbfun  18386  qtoptop2  23747  volf  25579  nolesgn2ores  27724  nosupres  27759  nosupbnd2lem1  27767  noetasuplem4  27788  noetainflem4  27792  oniso  28352  bdayn0sf1o  28451  uhgrspansubgrlem  29448  upgrres  29464  umgrres  29465  hlimf  31397  fsuppcurry1  32887  fsuppcurry2  32888  eulerpartlemmf  34633  eulerpartlemgvv  34634  bj-funidres  37604  imadomfi  42580  funcoressn  47597  fundmdfat  47684  afvelrn  47723  dmfcoafv  47730  aovmpt4g  47756  fundmafv2rnb  47785