Theorem funres 6580

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   ↾ cres 5653  Fun wfun 6531

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

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-res 5663  df-fun 6539

This theorem is used by:  funresd  6581  fores  6804  resfunexg  7219  funfvima  7234  funiunfv  7250  fprlem1  8311  smores  8353  smores2  8355  frfnom  8436  sbthlem7  9105  fsuppres  9378  ordtypelem4  9508  wdomima2g  9573  imadomg  10606  imadomnum  10607  hashres  14576  hashimarn  14578  setsfun  17342  setsfun0  17343  lubfun  18517  glbfun  18530  qtoptop2  24011  volf  25843  nolesgn2ores  28022  nosupres  28057  nosupbnd2lem1  28065  noetasuplem4  28086  noetainflem4  28090  oniso  28650  bdayn0sf1o  28749  uhgrspansubgrlem  29864  upgrres  29880  umgrres  29881  hlimf  31832  fsuppcurry1  33309  fsuppcurry2  33310  eulerpartlemmf  35000  eulerpartlemgvv  35001  bj-funidres  38052  imadomfi  43032  funcoressn  48081  fundmdfat  48168  afvelrn  48207  dmfcoafv  48214  aovmpt4g  48240  fundmafv2rnb  48269