Theorem funres 6578

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 5999	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6555	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3904   ↾ cres 5662  Fun wfun 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ss 3921  df-br 5109  df-opab 5173  df-rel 5667  df-cnv 5668  df-co 5669  df-res 5672  df-fun 6538

This theorem is used by:  funresd  6579  fores  6802  resfunexg  7213  funfvima  7228  funiunfv  7246  fprlem1  8295  smores  8337  smores2  8339  frfnom  8420  sbthlem7  9079  fsuppres  9351  ordtypelem4  9481  wdomima2g  9546  imadomg  10524  hashres  14482  hashimarn  14484  setsfun  17237  setsfun0  17238  lubfun  18412  glbfun  18425  qtoptop2  23867  volf  25699  nolesgn2ores  27847  nosupres  27882  nosupbnd2lem1  27890  noetasuplem4  27911  noetainflem4  27915  oniso  28475  bdayn0sf1o  28574  uhgrspansubgrlem  29651  upgrres  29667  umgrres  29668  hlimf  31600  fsuppcurry1  33080  fsuppcurry2  33081  eulerpartlemmf  34774  eulerpartlemgvv  34775  bj-funidres  37823  imadomfi  42797  funcoressn  47807  fundmdfat  47894  afvelrn  47933  dmfcoafv  47940  aovmpt4g  47966  fundmafv2rnb  47995