Theorem funres 6610

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ↾ cres 5660  Fun wfun 6560

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-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-br 5109  df-opab 5174  df-rel 5665  df-cnv 5666  df-co 5667  df-res 5670  df-fun 6568

This theorem is used by:  funresd  6611  fores  6836  resfunexg  7252  funfvima  7267  funiunfv  7283  fprlem1  8356  smores  8398  smores2  8400  frfnom  8481  sbthlem7  9150  fsuppres  9422  ordtypelem4  9552  wdomima2g  9617  imadomg  10652  imadomnum  10653  hashres  14624  hashimarn  14626  setsfun  17393  setsfun0  17394  lubfun  18574  glbfun  18587  qtoptop2  24073  volf  25905  nolesgn2ores  28086  nosupres  28121  nosupbnd2lem1  28129  noetasuplem4  28150  noetainflem4  28154  oniso  28714  bdayn0sf1o  28813  uhgrspansubgrlem  29928  upgrres  29944  umgrres  29945  hlimf  31896  fsuppcurry1  33412  fsuppcurry2  33413  eulerpartlemmf  35118  eulerpartlemgvv  35119  srepdflem1  36126  bj-funidres  38340  imadomfi  43318  funcoressn  48385  fundmdfat  48472  afvelrn  48511  dmfcoafv  48518  aovmpt4g  48544  fundmafv2rnb  48573