Theorem funres 6575

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-res 5667  df-fun 6535

This theorem is used by:  funresd  6576  fores  6799  resfunexg  7214  funfvima  7229  funiunfv  7245  fprlem1  8299  smores  8341  smores2  8343  frfnom  8424  sbthlem7  9091  fsuppres  9363  ordtypelem4  9493  wdomima2g  9558  imadomg  10537  imadomnum  10538  hashres  14503  hashimarn  14505  setsfun  17263  setsfun0  17264  lubfun  18438  glbfun  18451  qtoptop2  23925  volf  25757  nolesgn2ores  27908  nosupres  27943  nosupbnd2lem1  27951  noetasuplem4  27972  noetainflem4  27976  oniso  28536  bdayn0sf1o  28635  uhgrspansubgrlem  29750  upgrres  29766  umgrres  29767  hlimf  31718  fsuppcurry1  33195  fsuppcurry2  33196  eulerpartlemmf  34886  eulerpartlemgvv  34887  bj-funidres  37903  imadomfi  42868  funcoressn  47930  fundmdfat  48017  afvelrn  48056  dmfcoafv  48063  aovmpt4g  48089  fundmafv2rnb  48118